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]