Generative unbinding of names

10 years 12 months ago
Generative unbinding of names
This paper is concerned with a programming language construct for typed name binding that enforces -equivalence. It proves a new result about what operations on names can co-exist with this construct. The particular form of typed name binding studied is that used by the FreshML family of languages. Its characterisure is that a name binding is represented by an abstract (name,value)-pair that may only be deconstructed via the generation of fresh bound names. In FreshML the only observation one can make of names is to test whether or not they are equal. This restricted amount of observation was thought necessary to ensure that there is no observable difference between -equivalent name binders. Yet from an algorithmic point of view it would be desirable to allow other operations and relations on names, such as a total ordering. This paper shows that, contrary to expectations, one may add not just ordering, but almost any relation or numerical function on names without disturbing the fund...
Andrew M. Pitts, Mark R. Shinwell
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where POPL
Authors Andrew M. Pitts, Mark R. Shinwell
Comments (0)