Mechanizing the Metatheory of LF
- 1 June 2008
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2008 23rd Annual IEEE Symposium on Logic in Computer Science
Abstract
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments. Although detailed informal proofs of these properties have been published, they have not been formally verified in a theorem prover. We have formalized these properties within Isabelle/HOL using the nominal datatype package, closely following a recent article by Harper and Pfenning. In the process, we identified and resolved a gap in one of the proofs and a small number of minor lacunae in others. Besides its intrinsic interest, our formalization provides a foundation for studying the adequacy of LF encodings, the correctness of Twelf-style metatheoretic reasoning, and the metatheory of extensions to LF.Keywords
Other Versions
This publication has 15 references indexed in Scilit:
- Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence CheckingElectronic Notes in Theoretical Computer Science, 2008
- Engineering formal metatheoryPublished by Association for Computing Machinery (ACM) ,2008
- Barendregt’s Variable Convention in Rule InductionsLecture Notes in Computer Science, 2007
- Proof Pearl: De Bruijn Terms Really Do WorkLecture Notes in Computer Science, 2007
- Mechanizing metatheory in a logical frameworkJournal of Functional Programming, 2007
- Nominal Techniques in Isabelle/HOLLecture Notes in Computer Science, 2005
- A Trustworthy Proof CheckerJournal of Automated Reasoning, 2003
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- A verified typecheckerPublished by Springer Science and Business Media LLC ,1995
- An algorithm for testing conversion in type theoryPublished by Cambridge University Press (CUP) ,1991