coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Formalization of Ott alpha-equivalence?

From: Mitchell Wand <wand AT ccs.neu.edu>
To: coq-club AT inria.fr, Peter.Sewell AT cl.cam.ac.uk
Subject: [Coq-Club] Formalization of Ott alpha-equivalence?
Date: Tue, 11 Mar 2014 10:17:52 -0400

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

[Coq-Club] Formalization of Ott alpha-equivalence?, Mitchell Wand, 03/11/2014
- Re: [Coq-Club] Formalization of Ott alpha-equivalence?, Francesco Zappa Nardelli, 03/12/2014
  - Re: [Coq-Club] Formalization of Ott alpha-equivalence?, Mitchell Wand, 03/12/2014
- Re: [Coq-Club] Formalization of Ott alpha-equivalence?, Frédéric Blanqui, 03/12/2014