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

Below is a list of available implementations of lambda Prolog.


Gopalan Nadathur, along with some students and colleagues, has designed and implemented an abstract machine and compiler for lambda Prolog. That compiler, called Teyjus, is distributed in C and has been available as a beta release starting in the summer of 1999. This is the best and most up-to-date implementation of lambda Prolog available.


Terzo is an interpreter of lambda Prolog implemented in Standard ML of NJ implementation. This interpreter is the third in a sequence of lambda 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 lambda 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 lambda 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