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]