Engineering formal metatheory

9 years 2 months ago
Engineering formal metatheory
Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. The representation and manipulation of terms with variable binding is a key issue. We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, ...). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defi...
Arthur Charguéraud, Benjamin C. Pierce, Bri
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where POPL
Authors Arthur Charguéraud, Benjamin C. Pierce, Brian E. Aydemir, Randy Pollack, Stephanie Weirich
Comments (0)