# A Metalanguage for Programming with Bound Names Modulo
Renaming

#### Andrew M. Pitts,
Cambridge University Computer Laboratory,
Pembroke Street Cambridge CB2 3QG, UK

#### Joint work with Murdoch J. Gabbay, DPMMS,
Cambridge University, Cambridge CB2 1SB, UK

### Abstract

This talk 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 [Gabbay and
Pitts, Proc. LICS '99, pp~214--224]. 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.

[slides]