The Coq mailing list

[Francesco Zappa Nardelli <francesco.zappa_nardelli AT inria.fr>]

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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail