http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM7Weirich2WG211/M7Weirich2 - Revision history2026-04-05T21:08:50ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M7Weirich2&diff=259&oldid=prevAdmin: 1 revision2011-12-12T10:06:28Z<p>1 revision</p>
<p><b>New page</b></p><div>[[Category:WG211]]<br />
<br />
<br />
<h1>LNgen: Tool Support for Locally Nameless Representations</h1><br />
<h3>Stephanie Weirich and Brian Aydemir</h3><br />
<br />
Abstract: Given the complexity of the metatheoretic reasoning involved<br />
with current programming languages and their type systems, techniques<br />
for mechanical formalization and checking of the metatheory have<br />
received much recent attention. In previous work [1], we advocated a<br />
combination of locally nameless representation and cofinite<br />
quantification as a lightweight style for carrying out such<br />
formalizations in the Coq proof assistant. As part of the<br />
presentation of that methodology, we described a number of operations<br />
associated with variable binding and listed a number of properties,<br />
called ``infrastructure lemmas,'' about those operations that needed<br />
to be shown. The proofs of these infrastructure lemmas are generally<br />
straightforward, given a specification of the binding structure of the<br />
language.<br />
<br />
In this work, we present LNgen [2], a prototype tool for automatically<br />
generating these definitions, lemmas, and proofs from Ott-like<br />
language specifications [3]. Furthermore, the tool also generates a<br />
recursion scheme for defining functions over syntax, which was not<br />
available in our previous work. We also show the soundness and<br />
completeness of our tool's output. For untyped lambda terms, we prove<br />
the adequacy of our representation with respect to a fully concrete<br />
representation, and we argue that the representation is complete<br />
----<br />
that we generate the right set of lemmas<br />
----<br />
with respect to Gordon and<br />
Melham's ``Five Axioms of Alpha-Conversion.'' Finally, we claim that<br />
our recursion scheme is simpler to work with than either Gordon and<br />
Melham's recursion scheme or the recursion scheme of Nominal Logic.<br />
<br />
[1] Engineering Formal Metatheory, POPL '08. With Arthur Chargu�raud,<br />
Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich.<br><br />
[2] http://www.cis.upenn.edu/~baydemir/papers/lngen/<br><br />
[3] http://www.cl.cam.ac.uk/~pes20/ott/</div>Admin