Polymorphic lemmas and definitions in λProlog and Twelf

Andrew W. Appel, Amy P. Felty

Research output: Contribution to journalArticlepeer-review

3 Scopus citations


λProlog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage (λProlog). We discuss both the Terzo and Teyjus implementations of λProlog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.

Original languageEnglish (US)
Pages (from-to)1-39
Number of pages39
JournalTheory and Practice of Logic Programming
Issue number1-2
StatePublished - 2004

All Science Journal Classification (ASJC) codes

  • Software
  • Artificial Intelligence
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computational Theory and Mathematics


  • Lambda Prolog
  • Twelf
  • definitions
  • higher-order logic programming
  • lemmas
  • logical frameworks
  • polymorphism
  • proof-carrying code
  • theorem proving


Dive into the research topics of 'Polymorphic lemmas and definitions in λProlog and Twelf'. Together they form a unique fingerprint.

Cite this