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
defined using cofinite quantification are strong enough for metatheoretic
reasoning, and need not be explicitly strengthened. Strong
inversion principles follow (automatically, in Coq) from the induction
principles. Although many of the underlying ingredients of our
technique have been used before, their combination here yields a
significant improvement over other methodologies using first-order
representations, leading to developments that are faithful to informal
practice, yet require no external tool support and little infrastructure
within the proof assistant.
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 Fsub
and core ML (with references, exceptions, datatypes, recursion, and
patterns) and subject reduction for the Calculus of Constructions.
Not only do these developments demonstrate the comprehensiveness
of our approach; they have also been optimized for clarity and
robustness, making them good templates for future extension.
