https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/

lProlog: Logic programming in higher-order logic

lProlog 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 lProlog 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 lProlog
contain support for simply typed l-terms and (subsets) of
higher-order unification. As a result, lProlog was the world's first
programming language to directly support higher-order abstract syntax
(HOAS).

Although lProlog 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 lProlog

 1. Enrico Tassi and his colleagues are actively developing ELPI: an
    embeddable lProlog interpreter. Version 3.4.5 was released on 11
    December 2025. The interpreter is written in OCaml and it is
    described in a paper that appeared in LPAR 2015. The Coq plugin
    Coq-ELPI makes it possible to execute lProlog 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 lProlog. 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 lProlog. Makam is implemented from scratch in
    OCaml.

Language documentation

Document of lProlog 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 lProlog and to higher-order logic programming.
    Some additional YouTube videos related to lProlog are also
    available.
  * Alwen Tiu has course material on Programming in Higher-Order
    Logic (2009).
  * Amy Felty has written a tutorial on lProlog and its Applications
    to Theorem Proving (1997).
  * Olivier Ridoux has written Lambda-Prolog de A a Z... ou presque
    (163 pages, French, 1998).
  * John Hannan has written a tutorial on Program Analysis in lProlog
    at the 1998 PLILP Conference.
  * There is a bibliography that includes papers on the theory,
    design, applications, and implementation of lProlog 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
lProlog (and linear logic extensions of it) are described in detail.

[logo-small]  : a prover for lProlog 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 l-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 lProlog. Abella's logic then
serves as the reasoning logic. Probably the most elegant
formalization of the p-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 lProlog 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 lProlog programs in a web
browser: for an example, see the online MLTS implementation.

---------------------------------------------------------------------
Last updated: 12 December 2025