λProlog: Logic programming in higher-order logic

λ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 world's 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.

Current implementations of λProlog

1. Enrico Tassi and his colleagues are actively developing ELPI: an embeddable λProlog interpreter. Version 2.0.6 was released on 13 December 2024. The interpreter is written in OCaml and it is described in a paper that appeared LPAR 2015. The Coq plugin Coq-ELPI makes it possible to execute λProlog programs in a Coq environment. See Enrico's Tutorial on the ELPI programming language.
2. Gopalan Nadathur and his team have developed the Teyjus implementation of λProlog. Version 2.1.1 was released on 8 February 2023. The Teyjus compiler is written in OCaml, and it now supports separate computation, effective uses of types at run-time, a restriction of unification to the higher-order pattern fragment, etc. The ALP Newsletter (March 2010) has an overview article about the Teyjus system.
3. Antonis Stampoulis has implemented the Makam metalanguage which is a refinement of λProlog. Makam is implemented from scratch in OCaml.

Language documentation

Document of λProlog and its applications are available from a number of sources.

• Dale Miller and Gopalan Nadathur have written the book Programming with Higher-Order Logic (2012) which focuses on using logic programs in higher-order logic to provide declarative specifications for a range of applications. The book is available from CUP, Amazon.com, Amazon.fr, and eBooks.
• Zakaria Chihani has a series of video tutorials providing an introduction to λProlog and to higher-order logic programming. Some additional YouTube videos related to λProlog are also available.
• Alwen Tiu has course material on Programming in Higher-Order Logic (2009).
• Amy Felty has written a tutorial on λProlog and its Applications to Theorem Proving (1997).
• Olivier Ridoux has written Lambda-Prolog de A à Z... ou presque (163 pages, French, 1998).
• John Hannan has written a tutorial on Program Analysis in λProlog at the 1998 PLILP Conference.
• There is a bibliography that includes papers on the theory, design, applications, and implementation of λProlog from between 1985 and 2000.

 : a prover for λProlog programs

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 nominal variables; and
3. a built-in, two-level logic approach to reasoning about computation.

Examples of code

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.

The lprolog mailing list is closed

A mailing list for λProlog, most recently maintained by Gopalan Nadathur, has been closed after operating for about 25 years.