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.