λ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 is actively developing ELPI: an embeddable λProlog interpreter. Version 1.18.2 was released on 12 January 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.

 : 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.
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: 30 November 2023