[TYPES/announce] Paper announcement: Mechanizing the Metatheory of LF

[James Cheney]

On behalf of co-authors Christian Urban and Stefan Berghofer, we are
happy to announce the availability of the following technical report.
This an extended version of a paper to appear in LICS 2008.  Comments
are very welcome.

--James Cheney

http://arxiv.org/abs/0804.1667

Mechanizing the Metatheory of LF

Christian Urban, James Cheney and Stefan Berghofer

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.