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
Examples, including sample Ott specifications and the resulting outputs from Ott and LNgen, are included with the LNgen distribution.
Download
- Dependencies:
- GHC version 6.10. Other Haskell compilers may work, but they are untested.
- Ott version 0.10.16 or 0.10.17. Note: LNgen currently requires that you patch Ott, so you must install Ott from source.
- Penn's metatheory library. A copy is included with LNgen.
- Releases (detailed change log):
- lngen-0.3.tar.gz (2009-10-13)
- lngen-0.2.tar.gz (2009-07-14)
- lngen-0.1.tar.gz
(2009-03-06)