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.

References in zbMATH (referenced in 17 articles )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification: extended pattern unification (2022)
  2. Miller, Dale: Mechanized metatheory revisited (2019)
  3. Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
  4. Miller, Dale: Proof checking and logic programming (2017)
  5. Ahn, Ki Yung; Vezzosi, Andrea: Executable relational specifications of polymorphic type systems using Prolog (2016)
  6. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification (2016)
  7. Dunchev, Cvetan; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico: ELPI: fast, embeddable, (\lambda)Prolog interpreter (2015)
  8. Miller, Dale: Proof checking and logic programming (2015)
  9. Steen, Alexander; Benzmüller, Christoph: There is no best (\beta)-normalization strategy for higher-order reasoners (2015)
  10. Wisniewski, Max; Steen, Alexander; Benzmüller, Christoph: \textscLeoPARD-- a generic platform for the implementation of higher-order reasoners (2015)
  11. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  12. Miller, Dale: A proposal for broad spectrum proof certificates (2011)
  13. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Reasoning in Abella about structural operational semantics specifications (2009)
  14. Liang, Chuck; Nadathur, Gopalan; Qi, Xiaochu: Choices in representation and reduction strategies for lambda terms in intensional contexts (2004)
  15. Pientka, Brigitte; Pfenning, Frank: Optimizing higher-order pattern unification. (2003)
  16. Nadathur, Gopalan: The suspension notation for lambda terms and its use in metalanguage implementations (2002)
  17. Miller, Dale: Encoding generic judgments: preliminary results (2001)