In 2005, based on the observation that no existing technique was practical and general enough for formally reasoning about binders, a number of researchers proposed the POPLMark challenge as a way to stimulate new research on the topic (Aydemir et al 2005). This challenge, which received a lot of attention in the community, led to two the development of two new approaches: the nominal approach, mainly developed by Urban (2005), and another approach called locally nameless with cofinite quantification. I have developed the latter during an internship at UPenn in 2006, with Benjamin Pierce and Stephanie Weirich as advisors. Brian Aydemir and Randy Pollack then joined us in 2007 and contributed to the formal developments and to the proof of adequacy, respectively.

The second ingredient is the cofinite quantification, which plays a key role in making it possible to directly obtain strong induction principles. Without it, a large number of renaming lemmas are required, as experienced by Leroy in his POPLMark solution. The cofinite quantification plays a similar role as in Gabbay and Pitts' nominal logic (1999), with the difference that it is here used in a standard logic and that is is introduced directly in inductive definitions.

The particular way in which we combine these two ingredients leads to concise developments that remain quite faithful to the presentation of conventional paper proofs. We have illustrated the applicability of this technique on four major developments: the formalization of ML with datatypes, references and exceptions, the formalization of System F with subtyping, the formalization of the Calculus of Constructions, and the formalization of the CPS translation. The locally nameless approach has already been adopted by dozens of researchers. A non-exhaustive list can be found at the bottom of this page.