Archive for the 'Locally nameless' Category

LNGen: Tool Support for Locally Nameless Representations

By Brian Aydemir and Stephanie Weirich, preprint, available from Brian Aydemir’s website:

Given the complexity of the metatheoretic reasoning about current programming languages and their type systems, techniques for mechanical formalization and checking of such metatheory have received
much recent attention. In previous work, we advocated a combination of locally nameless representation and cofinite quantification as a light- weight style for carrying out such formalizations in the Coq proof assistant. As part of the presentation of that methodology, we described a number of operations associated with variable binding and listed a number of properties, called “infrastructure lemmas”, about those operations that needed to be shown. The proofs of these infrastructure lemmas are straightforward but tedious.
In this work, we present LNgen, a prototype tool for automatically generating statements and proofs of infrastructure lemmas from Ott language specifications. Furthermore, the tool also generates a recursion scheme for defining functions over syntax, which was not available in our previous work. LNgen works in concert with Ott to effectively alleviate much of the tedium of working with locally nameless syntax. For the case of untyped lambda terms, we show that the combined output from the two tools is sound and complete, with LNgen automatically proving many of the key lemmas. We prove the soundness of our representation with respect to a fully concrete representation, and we argue that the representation is complete—that we generate the right set of lemmas—with respect to Gordon and Melham’s “Five Axioms of Alpha-Conversion.”

Associated Coq code can be found here.


I am not a number: I am a free variable

By Conor McBride and James McKinna, from Haskell Workshop 2004, available from Conor McBride’s website:

In this paper, we show how to manipulate syntax with binding using a mixed representation of names for free variables (with respect to the task in hand) and de Bruijn indices [5] for bound variables. By doing so, we retain the advantages of both representations: naming supports easy, arithmetic-free manipulation of terms; de Bruijn indices eliminate the need for α-conversion. Further, we have ensured that not only the user but also the implementation need never deal with de Bruijn indices, except within key basic operations.

Moreover, we give a hierarchical representation for names which naturally reflects the structure of the operations we implement. Name choice is safe and straightforward. Our technology combines easily with an approach to syntax manipulation inspired by Huet’s ‘zippers'[10].Without the ideas in this paper, we would have struggled to implement EPIGRAM [19]. Our example-constructing inductive elimination operators for datatype families-is but one of many where it proves invaluable.