λProlog is a logic programming language based on an intuitionistic fragment 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.
Although λProlog was originally designed and implemented in the late 1980s, interest in the language contains 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:
A mailing list for λProlog, most recently maintained by Gopalan Nadathur, has been closed after operating for about 25 years.