The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

Dear all,

Stephanie Weirich and I would like to announce LNgen, a prototype tool  
for generating Coq code for the infrastructure associated with a  
locally nameless representation.  This work builds upon our work with  
Charguéraud, Pierce, and Pollack on Engineering Formal Metatheory,  
where we described a locally nameless strategy for representing  
languages with binding.

LNgen uses a subset of the Ott specification language [1] as its input  
language.  Currently, it supports the definition of syntax with single  
binders.  Compared to the recently announced locally nameless backend  
for Ott [2], LNgen does not handle the definition of relations, but it  
does generate a large collection of "infrastructure" lemmas and their  
proofs, e.g., facts about substitution.

You can read more about the tool and download it from

        http://www.cis.upenn.edu/~baydemir/papers/lngen/

Cheers,
Brian and Stephanie

[1] http://www.cl.cam.ac.uk/~pes20/ott/

[2] http://moscova.inria.fr/~zappa/projects/ln_ott/