I have worked on the locally nameless approach to representing syntax with variable bindings. This technique has shown very useful to carrying out mechanized proofs of results from programming language metatheory, e.g. type soundness proofs. The locally nameless representation avoids issues related to alpha-conversion by using de Bruijn indices for bound variables, and avoids issues related to shifting of de Bruijn indices by using names to represent free variables. One key ingredient that I have exploited is the cofinite quantification of free variables names in inductive definitions. This cofinite quantification leads to the generation of strong induction principles, while still offering sufficient flexibility in the choice of fresh names. The combination of locally nameless representation with cofinite quantification has been used to formalize large amount of metatheory, including proofs of type soundness for System-F, for mini-ML, for the Calculus of Construction, as well as proofs of the Church-Rosser property for the lambda-calculus and proof of semantic-preservation of the CPS transformation.

This work is in the line with the POPLMark Challenge. It originates in a 5-month internship that I completed at the University of Pennsylvania, advised by Stephanie Weirich and Benjamin C. Pierce. Later, Brian Aydemir and Randy Pollack joined our team.

For an introduction to the locally nameless representation with cofinite quantification, read The Locally Nameless Representation, by Arthur Charguéraud (JAR, to appear) To learn more about the justification of the cofinite quantification, about case studies and comparison with other approaches to representating variable bindings, read Engineering Formal Metatheory, by Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack and Stephanie Weirich (POPL'08).