Lambda the Ultimate

Aydemir, Charguéraud, Pierce, Pollack, and Weirich. 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, . . . ).

...

We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F_<: and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions.

A fairly recent paper from the POPLmark team, which describes an approach to formalizing programming metatheory that they think performs well on the POPLmark challenge criteria (low formalization overhead, low cost of entry, and reasonable similarity to existing informal proof techniques). It looks like this is related to some of the material presented in the How to write your next POPL paper in Coq tutorial at POPL'08, which was previously mentioned on LtU.