System description: teyjus-a compiler and abstract machine based implementation of #lambda# prolog

摘要

The logic programming language #lambda# Prolog is based on the inuitionistic theory of higher- order hereditary Harrop formulas, a logic that significantly extends the theory of Horn clauses. A systematic exploitation of features in the richer logic endows #lambda# Prolog with capabilities at the programming level that are not present in traditional logic programming languages. Severla studies have established the value of #lambda# Prolog as a language for implementing systems that manipulate formal objects such as formulas, programs, proofs and types. Towards harnessing these benefits, methods have been developed for realizing this language efficiently. This work has culminated in the description of an abstract machine and compiler based implementation scheme. An actual implementation of #lambda# Prolog based on these ideas has recently been completed. The planned presentation will exhibit this system-called Teyjus-and will also illuminate the metalanguage capabilities of #lambda# Prolog.