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.
Related papers
- LNgen: Tool Support for Locally Nameless Representations [draft] (with Stephanie Weirich)
- Engineering Formal Metatheory [POPL 2008] (with Arthur Chargéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich)
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.
-
Current release (detailed change log):
- lngen-0.3.tar.gz (2009-10-13, version 0.3)
-
Local closure predicates are generated for
both
PropandSet. -
Theorems are stated using the version in
Prop.
-
Older releases:
- lngen-0.2.tar.gz (2009-07-14, version 0.2)
- lngen-0.1.tar.gz (2009-03-06, version 0.1)