Back to the FAQ / Home
What implementations of λProlog are available?

Below is a list of available implementations of λProlog as of May 2020.


Enrico Tassi and his colleagues have developed the ELPI implementation of λProlog. The system is written in Ocaml and is designed to be embeddable. In particular, it is used as part of the Coq-ELPI plugin for the Coq theorem prover. The code for both ELPI and Coq-ELPI are available on GitHub.


Gopalan Nadathur, along with some students and colleagues, has designed and implemented an abstract machine and compiler for λProlog. That compiler, called Teyjus, is distributed in C and has been available as a beta release starting in the summer of 1999. The source code for Teyjus Version 2 is available on GitHub.


Antonis Stampoulis has implemented the Makam metalanguage which is a refinement of λProlog. Makam is implemented from scratch in OCaml.


Terzo is an interpreter of λProlog implemented in Standard ML of NJ implementation. This interpreter is the third in a sequence of λProlog interpreters written and maintained by people from Bell Labs, Carnegie-Mellon, Duke University, and the University of Pennsylvania. More about it is available here.


The following description is taken from the Prolog FAQ.

Prolog/Mali is a compiler for the higher-order language Lambda-Prolog. Lambda-Prolog .... Prolog/Mali is a complete system which includes a C translator, a linker, libraries, runtime, and documentation, and runs on UNIX. It requires the MALI-V06 abstract memory package. Prolog/Mali is available by anonymous ftp from Written by Pascal Brisset ( (or and Olivier Ridoux ( To be added to the mailing list, send mail to For more information, send mail to

It can be found in the CMU Artificial Intelligence Repository.


Development of a Standard ML implementation of λProlog was started by Frank Pfenning (CMU) and later maintained and extended by Amy Felty (then at AT&T Bell Labs). This system has been used successfully by various students in their research and has been used in undergraduate courses to teach computational logic and automated deduction.

eLP: Ergo Lambda Prolog

eLP (Ergo Lambda Prolog) is an interpreter written by Conal Elliott, Frank Pfenning and Dale Miller in Common Lisp and implements the core of λProlog (higher-order hereditary Harrop formulas). It is embedded in a larger development environment called ESS (the Ergo Support System). eLP implements all core language feature and offers a module system, I/O, some facilities for tracing, error handling, arithmetic, recursive top-levels, on-line documentation and a number of extended examples, including many programs from Amy Felty's and John Hannan's thesis. It can be found in the CMU Artificial Intelligence Repository.


Miller and Nadathur collaborated on the Prolog implementations, LP2.6 and LP2.7, which have been available since 1987: these systems did not implement the full logic (in particular, implications in the body of clauses were not supported). Although the system is old (finished in July 1988), it might still be useful, especially for experimenting with higher-order unification and higher-order programming. It is available in C-Prolog and Quintus sources and was written by Dale Miller and Gopalan Nadathur. It can be found in the CMU Artificial Intelligence Repository as well as a compressed tar file.

Back to the FAQ / Home