System description: Teyjus—a compiler and abstract machine based implementation of λprolog

Gopalan Nadathur; Dustin J. Mitchell

doi:10.1007/3-540-48660-7_25

System description: Teyjus—a compiler and abstract machine based implementation of λprolog

Gopalan Nadathur, Dustin J. Mitchell

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

62 Scopus citations

Abstract

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
Editors	Harald Ganzinger
Publisher	Springer Verlag
Pages	287-291
Number of pages	5
ISBN (Print)	3540662227, 9783540662228
DOIs	https://doi.org/10.1007/3-540-48660-7_25
State	Published - 1999
Event	16th International Conference on Automated Deduction, CADE 1999 - Trento, Italy Duration: Jul 7 1999 → Jul 10 1999

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1632
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	16th International Conference on Automated Deduction, CADE 1999
Country/Territory	Italy
City	Trento
Period	7/7/99 → 7/10/99

Bibliographical note

Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.

Access

10.1007/3-540-48660-7_25

OpenUrl availability

Full text

Cite this

Nadathur, G., & Mitchell, D. J. (1999). System description: Teyjus—a compiler and abstract machine based implementation of λprolog. In H. Ganzinger (Ed.), Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings (pp. 287-291). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1632). Springer Verlag. https://doi.org/10.1007/3-540-48660-7_25

System description: Teyjus—a compiler and abstract machine based implementation of λprolog. / Nadathur, Gopalan; Mitchell, Dustin J.
Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings. ed. / Harald Ganzinger. Springer Verlag, 1999. p. 287-291 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1632).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Nadathur, G & Mitchell, DJ 1999, System description: Teyjus—a compiler and abstract machine based implementation of λprolog. in H Ganzinger (ed.), Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1632, Springer Verlag, pp. 287-291, 16th International Conference on Automated Deduction, CADE 1999, Trento, Italy, 7/7/99. https://doi.org/10.1007/3-540-48660-7_25

Nadathur G, Mitchell DJ. System description: Teyjus—a compiler and abstract machine based implementation of λprolog. In Ganzinger H, editor, Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1999. p. 287-291. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-48660-7_25

Nadathur, Gopalan ; Mitchell, Dustin J. / System description : Teyjus—a compiler and abstract machine based implementation of λprolog. Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings. editor / Harald Ganzinger. Springer Verlag, 1999. pp. 287-291 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3eb7d7544fe44bc09f2500d48d276948,

title = "System description: Teyjus—a compiler and abstract machine based implementation of λprolog",

abstract = "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.",

author = "Gopalan Nadathur and Mitchell, {Dustin J.}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 16th International Conference on Automated Deduction, CADE 1999 ; Conference date: 07-07-1999 Through 10-07-1999",

year = "1999",

doi = "10.1007/3-540-48660-7_25",

language = "English (US)",

isbn = "3540662227",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "287--291",

editor = "Harald Ganzinger",

booktitle = "Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings",

}

TY - GEN

T1 - System description

T2 - 16th International Conference on Automated Deduction, CADE 1999

AU - Nadathur, Gopalan

AU - Mitchell, Dustin J.

PY - 1999

Y1 - 1999

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84957611918&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957611918&partnerID=8YFLogxK

U2 - 10.1007/3-540-48660-7_25

DO - 10.1007/3-540-48660-7_25

M3 - Conference contribution

AN - SCOPUS:84957611918

SN - 3540662227

SN - 9783540662228

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 287

EP - 291

BT - Automated Deduction — CADE-16 - 16th International Conference on Automated Deduction, Proceedings

A2 - Ganzinger, Harald

PB - Springer Verlag

Y2 - 7 July 1999 through 10 July 1999

ER -

System description: Teyjus—a compiler and abstract machine based implementation of λprolog

Abstract

Publication series

Other

Bibliographical note

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this