Polymorphic Lemmas and Definitions in λProlog and Twelf

Title: Polymorphic Lemmas and Definitions in λProlog and Twelf

Research Question: How can we implement polymorphic lemmas and definitions in λProlog and Twelf, two popular higher-order logic programming languages?

Methodology: We encoded 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 discussed both the Terzo and Teyjus implementations of λProlog and compared the features of the two metalanguages for our purposes.

Results: We presented a concise, informative summary suitable for a wiki entry from the research article. We demonstrated a definition /lemma implementation that is about three dozen lines of code. We also included a detailed comparison of the Twelf and λProlog versions of the encoding of our logic, lemmas, and definitions.

Implications: The research highlights the importance of polymorphic lemmas and definitions in implementing higher-order logics. It also emphasizes the role of language features in creating a small TCB and efficient representation of proofs. The comparison of programming issues in λProlog and Twelf provides valuable insights for developers working in these languages, particularly those working on proof-carrying code applications.

Link to Article: https://arxiv.org/abs/0403010v1 Authors: arXiv ID: 0403010v1