LNgen generates locally nameless infrastructure for the Coq proof assistant from Ott-like specifications. Its output is based on the locally nameless style advocated in Engineering Formal Metatheory and includes all of the "infrastructure" lemmas associated with that style. Compared to Ott's locally nameless back end, LNgen favors generating a large collection of infrastructure lemmas over handling complex binding specifications and methods of defining syntax and relations.

The author of the LNgen tool is Brian Aydemir. This project is no longer being maintained.

Related papers


Examples, including sample Ott specifications and the resulting outputs from Ott and LNgen, are included with the LNgen distribution.