Description:

Teyjus is an efficient implementation of the higher-order logic programming
language Lambda Prolog. One of the main strengths of Lambda Prolog, a language
originally 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 objects such as formulas and programs. Lambda Prolog
realizes this facility by employing data structures based on lambda terms to
represent the notion of binding 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.