Locally nameless representation with cofinite quantification
The locally nameless representation with cofinite quantification is a pratical technique for representing binders in a formal settings. The locally nameless representation avoids the need for alpha-conversion and the need for shifting de Bruijn indices. The cofinite quantification is used to obtain strong induction principles. On this page, you willl find a collection of examples formalized in Coq using this approach.
Engineering Formal Metatheory
with B. Aydemir, B. C. Pierce, R. Pollack and S. Weirich
Symposium on Principles of Programming Languages (POPL), January 2008
The Locally Nameless Representation
Journal of Automated Reasoning (JAR), May 2011
Details on tactics and automation techniques used above can be found here.
Additional tutorial examples
I maintain a non-exhaustive list of users.