The Coq mailing list

[Mitchell Wand <wand AT ccs.neu.edu>]

Ahh, thanks.  That looks very useful.

--Mitch

On Wed, Mar 12, 2014 at 4:14 PM, Francesco Zappa Nardelli <francesco.zappa_nardelli AT inria.fr> wrote:

Hi Mitch,

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.

That semantics of the binding structures of Ott is described in detail
in the note:

 http://www.cl.cam.ac.uk/~pes20/ott/bind-doc.pdf

with definitions formalised in Ott itself and paper proofs of some
sanity properties.  It should be easy to generate a Coq version of the
definitions  - we did some work towards that at the time, and we could
give you the Ott sources if you want.   But we didn't do mechanised
proofs of the metatheory.

-francesco