Showing cs.LOShow all
3 papers · 1 filter
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.LO2023
A Logical Framework with Infinitary Terms
Zhibo Chen
Logical frameworks are successful in modeling proof systems. Recently, CoLF extended the logical framework LF to support higher-order rational terms that enable adequate encoding o…
cs.LO2023
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…