Home

LNGen

LNGen

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 backend, LNgen favors generating a large collection of infrastructure lemmas over handling complex binding specifications and methods of defining syntax and relations.

There are really three stories here:

  1. Coq 8.2 shipped a while ago.
  2. Ott, a tool for PLT semantics work, has acquired a backend in support of the increasingly-popular "locally nameless" representation of binding structure in mechanized programming language metatheory.
  3. LNGen is another tool, using a subset of Ott syntax, that takes a slightly different approach from Ott's new backend to addressing the same issues.

From the U. Penn folks who brought us the Coq tutorial at POPL '08.

By Paul Snively at 2009-05-07 20:28 | Implementation | Semantics | Software Engineering | Type Theory | other blogs | 7504 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Fabulous

This is fabulous news. I was doing a lot of this myself and in a messier way. I'm glad to have a library to use so I can focus on the research rather than the infrastructure.

By Gavin Mendel-Gleason at Thu, 2009-05-14 09:02 | login or register to post comments