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