The logic programming language λProlog is based on the intuitionistic 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 λProlog with capabilities at the programming level that are not present in traditional logic programming languages. Several studies have established the value of λ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 λ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 λProlog.
|Original language||English (US)|
|Title of host publication||Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings|
|Number of pages||5|
|ISBN (Print)||3540662227, 9783540662228|
|State||Published - 1999|
|Event||16th International Conference on Automated Deduction, CADE 1999 - Trento, Italy|
Duration: Jul 7 1999 → Jul 10 1999
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Other||16th International Conference on Automated Deduction, CADE 1999|
|Period||7/7/99 → 7/10/99|
Bibliographical notePublisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.