λProlog: Logic programming in higher-order logic

λProlog: Logic programming in higher-order logic

λProlog is a logic programming language based on higher-order intuitionistic logic in the style of Church's Simple Theory of Types. Such a strong logical foundation provides λProlog with logically supported notions of modular programming, abstract datatypes, higher-order programming, and the lambda-tree syntax approach to the treatment of bound variables in syntax. Implementations of λProlog contain support for simply typed λ-terms and (subsets) of higher-order unification. As a result, λProlog was the world's first programming language to directly support higher-order abstract syntax (HOAS).

Although λProlog was originally designed and implemented in the late 1980s (the first distributed version was written in Prolog in 1988), interest in the language continues with new implementations and new applications, particularly in the area of meta-programming.

Current implementations of λProlog

Language documentation

Document of λProlog and its applications are available from a number of sources.

Dale Miller has written the book Proof Theory and Logic Programming: Computation as Proof Search in which much of the proof theory behind λProlog (and linear logic extensions of it) are described in detail.

: a prover for λProlog programs

Abella is an interactive theorem prover based on a number of new ways to exploit inductive and coinductive reasoning with relations. Abella is well-suited for reasoning about specification that manipulate objects with binding since it contains the following three logically motivated features:

direct support of λ-tree syntax (sometimes also called HOAS); the ∇-quantifier and nominal variables; and a built-in, two-level logic approach to reasoning about computation.

... continue reading