The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi.

If you are looking for some formalizations of alpha-equivalence in Coq, 
you may be interested in the ones available in http://color.inria.fr: 
Church (1932), Curry and Feys (1958), Krivine (1993) and Gabbay and 
Pitts (1999), all proved equivalent (see directory Term/Lamba).

I also know some developments in Coq by Rene Vestergaard on one hand, 
and Dimitri Hendriks and Vincent van Oostrom on the other hand 
(http://www.phil.uu.nl/preprints/lgpr/).

Best regards,

Frédéric.

Le 11/03/2014 15:17, Mitchell Wand a écrit :
> The JFP version (JFP 2010) of the Ott paper (ICFP 2007) contains a 
> worked-out definition of alpha-equivalence for terms whose binding 
> structures are defined in Ott.
>
> Does anybody know if this definition has been formalized in Coq or 
> some other theorem-prover?
>
> --Mitch