Mechanizing the Metatheory of LF

Christian Urban, James Cheney, Stefan Berghofer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

LF is a dependent type theory in which many other formal??systems canbe 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.
Original languageEnglish
Title of host publicationLogic in Computer Science
Subtitle of host publication2008 23rd Annual IEEE Symposium on Logic in Computer Science
Pages45-56
Number of pages12
Publication statusPublished - 2008

Keywords / Materials (for Non-textual outputs)

  • mechanized metatheory
  • logical frameworks
  • nominal logic

Fingerprint

Dive into the research topics of 'Mechanizing the Metatheory of LF'. Together they form a unique fingerprint.

Cite this