Clone this wiki locally
Teyjus - An Implementation of Lambda Prolog
The name "Teyjus" is used interchangeably for a family of systems and a project that are both about providing an efficient and robust implementation of the language Lambda Prolog. As a system, Teyjus has seen two incarnations. Its first version, released in mid-1999, was implemented entirely in C and supported full higher-order unification. Its second version, released in April 2008, is implemented in a mixture of C and OCaml and is oriented around a special form of higher-order unification known as pattern unification.
As a project, Teyjus has spanned a period of over a decade, involving, at various times, people from Duke University, SUNY Buffalo, the University of Chicago and the University of Minnesota; while the "project" was named only around 2000, its theme existed even earlier, and the system being distributed today reflects the cumulative result of all their efforts.
An attempt to list Lambda Prolog implementations
- LP2.6 (August 1987, Miller and Nadathur, University of Pennsylvania)
- LP2.7 (July 1988, Miller and Nadathur, Duke University and University of Pennsylvania). Available in C-Prolog and Quintus Prolog. 4100 lines of code. Does not implement the full dynamic module facility anticipated by the theory. Does provide a depth-first implementation of full higher-order unification.
- eLP (Winter 88 (?), Conal Elliott and Frank Pfenning, Carnegie-Mellon University). Written in Common Lisp. Used as a meta language within the ERGO program development project at Carnegie-Mellon. Implement the full theory of hohh as well as certain enhancements. This is the first practical version of λProlog.
- Prolog/MALI ~1992 (Olivier Ridoux, Pascal Brisset, Serge Le Huitouze, INRIA). First λProlog compiler available.
- Terzo (implemented in Standard ML) ~1997
- Teyjus Version 1, released in mid-1999, characterized by a complete support for the operation of higher-order unification. Implemented in C.
- Teyjus Version 2, released in April 2008, is oriented around a special form of higher-order unification known as pattern unification. The new version also includes modularity notions coupled with a complete form of separate compilation. Implemented in a mixture of C and OCaml.
- Abella - Interactive theorem prover based on lambda-tree syntax.
- Twelf and Twelf at Wikipedia - An implementation of the logical framework LF.
- Bedwyr - Allows model checking directly on syntactic expression possibly containing bindings.
- Lolli - Research language adding linear logic.
- Forum - Research language adding linear logic and concurrency.