Mechanizing the metatheory of LF
From MaRDI portal
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. We also formally derive a version of the type checking algorithm from which Isabelle/HOL can generate executable code. 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.
Recommendations
- Mechanizing metatheory in a logical framework
- Mechanized metatheory revisited
- A simplified account of the metatheory of linear LF
- Mechanizing the metatheory of Sledgehammer
- Towards a mechanized metatheory of Standard ML
- scientific article; zbMATH DE number 1303348
- Mechanizing metatheory without typing contexts
- A metatheory of a mechanized object theory
- A list-machine benchmark for mechanized metatheory
Cited in
(27)- Canonical HybridLF: extending Hybrid with dependent types
- Harpoon: mechanizing metatheory interactively
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Mechanized metatheory revisited
- Formalizing adequacy: a case study for higher-order abstract syntax
- Explicit contexts in LF (extended abstract)
- A simplified account of the metatheory of linear LF
- A bidirectional refinement type system for LF
- Structural recursion with locally scoped names
- Mechanised computability theory
- Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
- Mechanizing the metatheory of mini-XQuery
- Formalising Observer Theory for Environment-Sensitive Bisimulation
- Towards a mechanized metatheory of Standard ML
- The Isabelle Framework
- A coverage checking algorithm for LF
- scientific article; zbMATH DE number 1303348 (Why is no real title available?)
- αCheck: A mechanized metatheory model checker
- Mechanizing proofs with logical relations -- Kripke-style
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- POPLMark reloaded: mechanizing proofs by logical relations
- Formal SOS-Proofs for the Lambda-Calculus
- A proof-theoretic characterization of independence in type theory
- Mechanizing metatheory in a logical framework
- General bindings and alpha-equivalence in Nominal Isabelle
- A case study on logical relations using contextual types
- Universal Turing Machine
This page was built for publication: Mechanizing the metatheory of LF
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946633)
