λProlog Home Page (original) (raw)

λ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 thelambda-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.7 was released on 13 January 2025. 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 anoverview article about the Teyjus system.
3. Antonis Stampoulishas implemented the Makammetalanguage 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 Nadathurhave 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 fromCUP,Amazon.com, Amazon.fr, andeBooks.
• Zakaria Chihanihas 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 onProgramming 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.

Dale Miller has written the book Proof Theory and Logic Programming: Computation as Proof Search in which much of the proof theory behind λProlog (and linear logic extensions of it) are described in detail.

: a prover for λProlog programs

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

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.

Last updated: 12 May 2025