λ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.
A mailing list for λProlog, most recently maintained by Gopalan Nadathur, has been closed after operating for about 25 years.