2 papers
cs.LO2025
CoLF Logic Programming as Infinitary Proof Exploration
Zhibo Chen, Frank Pfenning
Logical Frameworks such as Automath [de Bruijn, 1968] or LF [Harper et al., 1993] were originally conceived as metalanguages for the specification of foundationally uncommitted ded…
cs.LO2025
A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
Zhibo Chen, Frank Pfenning
Higher-order unification has been shown to be undecidable. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has…