ΛProlog: Logic programming in higher-order logic
4 days ago
- #theorem proving
- #logic programming
- #higher-order logic
- λProlog is a logic programming language based on higher-order intuitionistic logic.
- It supports modular programming, abstract datatypes, higher-order programming, and lambda-tree syntax.
- First programming language to directly support higher-order abstract syntax (HOAS).
- Originally designed in the late 1980s, with continued interest in new implementations and applications.
- Dale Miller's book 'Proof Theory and Logic Programming' details the proof theory behind λProlog.
- Abella is an interactive theorem prover suited for reasoning about specifications with binding.
- Examples of λProlog code available in Teyjus distribution, book extracts, and online implementations.