λ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:
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.