λProlog: Logic programming in higher-order logic

λProlog is a logic programming language based on an intuitionistic fragment of Church's Simple Theory of Types. Such a strong logical foundations 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 implementations of the simply typed λ-terms as well as (subsets) of higher-order unification.

Current implementations of λProlog

  1. Gopalan Nadathur and his team have developed the Teyjus implementation of λProlog. Its 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.
  2. Claudio Sacerdoti Coen and Enrico Tassi have lead a team that developed ELPI: an embeddable λProlog interpreter. The interpreter is written in OCaml and it is described in a paper that appeared LPAR 2015.
  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 (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 implementaiton 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.

The lprolog mailing list

Gopalan Nadathur maintains the lprolog mailing list: visit https://wwws.cs.umn.edu/mm-cs/listinfo/lprolog to subscribe and to learn how to post. While this mailing list is mainly intended for the discussion of papers and systems concerning λProlog and related systems, announcements of conferences and workshops are also frequently posted there.


Last updated: 13 June 2018