Welcome to Teyjus

Teyjus is an efficient implementation of the declarative language Lambda Prolog. The main strength of Lambda Prolog, a language developed by Dale Miller and Gopalan Nadathur, is the support it offers for higher-order abstract syntax, a new and increasingly popular way to view the structure of complex syntactic objects such as types, formulas, proofs and programs. Lambda Prolog provides such 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 pose several implementation challenges that have been addressed in the work of Nadathur and his colleagues. The Teyjus system is a compiler and abstract machine based realization of Lambda Prolog that incorporates the ideas that have resulted from this research.

Further Information

Overview of the Teyjus system.
Download the latest version of the sources or an older version of the system.
Bug Tracking.
Language documentation.
Implementation documentation.
Project contributors.
External links.

Acknowledgments

Support for the work reported on this page and for the development of facilities that are available through it has been provided by the National Science Foundation under grants CCR-8905825, CCR-9208465, CCR-9596119, CCR-9803849, CCR-0096322 and CCF-0429572. 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.

Last updated by gopalan@cs.umn.edu on June 3, 2005