The Coq mailing list

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

Dear all,

we've recently extended our Ott tool to compile language definitions  
to a Coq representation in locally-nameless style with cofinite  
quantification, as popularised in Engineering Formal Metatheory by  
Aydemir, Charguéraud, Pierce, Pollack and Weirich. It deals with the  
single-binder case only.

Some examples (including STLC, Fsub, and the nu-calculus of Pitts and  
Stark) and the documentation are available from http:// 
moscova.inria.fr/~zappa/projects/ln_ott/ and the project web-site  
http://www.cl.cam.ac.uk/~pes20/ott/ ).

This is related to the recent LNgen tool of Aydemir and Weirich.   In  
broad terms, our extension compiles language definitions (including  
any inductively defined relations) but does not generate proof  
infrastructure for the language syntax, whereas LNgen generates proof  
infrastructure but does not currently support relation definitions.

Any feedback or comments would be very welcome.

Best wishes
        Francesco and Peter