A Meta Language for Programming with Bound Names Modulo
Renaming
Andrew M. Pitts and Murdoch J. Gabbay
Abstract
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 [Gabbay and Pitts 1999]. 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.