λProlog is a logic programming language based on an intuitionistic fragment of Church's Simple Theory of Types. Such a strong logical foundations 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 implementations of the simply typed λ-terms as well as (subsets) of higher-order unification.
Although λProlog was originally designed and implemented in the late 1980's, interest in the language contains with new implementations and new applications, particularly in the area of meta-programming.
Document of λProlog and its applications are available from a number of sources.
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: (1) direct support of λ-tree syntax (sometimes also called HOAS); (2) the ∇-quantifier; and (3) a built-in, two-level logic approach to reasoning about computation. In the latter feature, the specification logic is used to specify computations: this logic is a subset of λProlog. Abella's logic then serves as the reasoning logic. Probably the most elegant formalization of the π-calculus and its meta-theory is the one written in Abella. Principle contributors to the implementation of Abella are Kaustuv Chaudhuri, Andrew Gacek, and Yuting Wang.
Examples of λProlog code can be found various places: in the Teyjus distribution; in an extraction from the book Programming with Higher-Order Logic; and in a small collection. Since the ELPI implementation is written in OCaml and since OCaml can be compiled into JavaScript, it is possible to execute λProlog programs in a web browser: for an example, see the online MLTS implementation.
A mailing list for λProlog, most recently maintained by Gopalan Nadathur, has been closed after operating for about 25 years.