An efficient implementation of the higher-order logic programming language Lambda Prolog
C OCaml AMPL Perl C++ Standard ML Other
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.
emacs Updated the Teyjus emacs mode so that syntax highlighting properly Mar 26, 2009
examples The Makefile needed adjustment to not the situation where the make fa… Apr 15, 2008
lyacc Moved lyacc to the toplevel since it is a utility that users may want… Apr 11, 2008
scratch New scratch test for extending builtins. Oct 1, 2009
source Add string literals from proper character groups Feb 24, 2016
util Updated Ocamake so that it works with VS2008 and updated the README t… Mar 23, 2008
.gitignore Adding .gitignore Apr 18, 2016
COPYING Copying info. Mar 15, 2008
OMakeroot * Incremented the version number to 2.0-b2 Oct 27, 2008
QUICKSTART Rename README to QUICKSTART and create for GitHub Mar 20, 2015
RELEASE * Incremented the version number to 2.0-b2 Oct 27, 2008

The Teyjus system is an efficient implementation of the higher-order logic programming language Lambda Prolog. The main strength of Lambda Prolog, a language developed by Dale Miller and Gopalan Nadathur, is the support it offers for what is known as lambda tree syntax, a new and effective way to view the structure of complex syntactic objects such as types, formulas, proofs and programs. Lambda Prolog provides this support by using lambda terms as data representation devices and by including primitives for probing such terms in logically meaningful ways. The new features present in the language raise several implementation challenges that have been addressed in collaborative work between Nadathur and his students and colleagues. The name "Teyjus" actually stands both for a project and for a class of compiler and virtual machine based realizations of Lambda Prolog arising from the research carried out within this project. Underlying the most recent version of the Teyjus system is a new and significantly improved virtual machine that has been designed by Xiaochu Qi as part of her doctoral dissertation work at the University of Minnesota. This virtual machine extensively exploits a special form of higher-order unification known as pattern unification.


External Links


Support for the work reported on this page and for the development of facilities that are available through it has been provided primarily by the National Science Foundation under the grant CCF-0429572. This work is a continuation of earlier research funded by the NSF grants CCR-8905825, CCR-9208465, CCR-9596119, CCR-9803849 and CCR-0096322. Opinions, findings and conclusions or recommendations that are manifest in this material are those of the project participants and do not necessarily reflect the views of the NSF.