A metalanguage for programming with bound names modulo renaming

By Andrew M. Pitts and Murdoch J. Gabbay, from MPC 2000, available from Andrew M. Pitts’ website:

This paper describes work in progress on the design of an ML-style metalanguage FreshML for programming with recursively defined functions on user-defined, concrete data types whose constructors may involve variable binding. Up to operational equivalence, values of such FreshML data types can faithfully encode terms modulo alpha-conversion for a wide range of object languages in a straightforward fashion. The design of FreshML is `semantically driven’, in that it arises from the model of variable binding in set theory with atoms given by the authors in [7]. The language has a type constructor for abstractions over names (=atoms) and facilities for declaring locally fresh names. Moreover, recursive definitions can use a form of pattern-matching on bound names in abstractions. The crucial point is that the FreshML type system ensures that these features can only be used in well-typed programs in ways that are insensitive to renaming of bound names.

A Fresh Calculus for Name Management

By Davide Ancona and Eugenio Moggi, from GPCE 2004, available from Eugenio Moggi’s website:

We define a basic calculus for name management, which is obtained by an appropriate combination of three ingredients: extensible records (in a simplified form), names (as in FreshML), computational types (to allow computational effects, including generation of fresh names). The calculus supports the use of symbolic names for programming in-the-large, e.g. it subsumes Ancona and Zucca’s calculus for module systems, and for meta-programming (but not the intensional analysis of object level terms supported by FreshML), e.g. it subsumes (and improves) Nanevski and Pfenning’s calculus for meta-programming with names and necessity. Moreover, it models some aspects of Java’s class loaders.