Teyjus swMATH ID: 21364 Software Authors: Nadathur, G., Mitchell, D.J. Description: System description: Teyjus—a compiler and abstract machine based implementation of λ prolog. 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. Homepage: http://teyjus.cs.umn.edu/ Related Software: Twelf; Abella; Isabelle/HOL; Coq; Beluga; ELPI; Bedwyr; ML; Leo; Agda; Satallax; seL4; Nominal Isabelle; LCF; DRAT-trim; PoplMark; Nuprl; HYBRID; Leo-III; kepler98 Cited in: 17 Publications all top 5 Cited by 19 Authors 8 Miller, Dale Allen 4 Nadathur, Gopalan 2 Benzmüller, Christoph Ewald 2 Gacek, Andrew 2 Libal, Tomer 2 Steen, Alexander 1 Ahn, Ki Yung 1 Chihani, Zakaria 1 Dunchev, Cvetan 1 Guidi, Ferruccio 1 Liang, Chuck 1 Pfenning, Frank 1 Pientka, Brigitte 1 Qi, Xiaochu 1 Renaud, Fabien 1 Sacerdoti Coen, Claudio 1 Tassi, Enrico 1 Vezzosi, Andrea 1 Wisniewski, Max Cited in 3 Serials 4 Journal of Automated Reasoning 1 Formal Aspects of Computing 1 Annals of Mathematics and Artificial Intelligence Cited in 2 Fields 17 Computer science (68-XX) 10 Mathematical logic and foundations (03-XX) Citations by Year