A meta language for programming with bound names

The following preprint is available  electronically via:


and of course we'd welcome any comments.

Andy Pitts
Jamie Gabbay

A Meta Language for Programming with Bound Names Modulo Renaming
(Preliminary Report)

Andrew M. Pitts and Murdoch J. Gabbay


This paper describes work in progress on the design of an ML-style
meta language, FML, for programming with recursively defined functions
on user-defined data types whose constructors may involve variable
binding. Up to operational equivalence, values of such data types can
faithfully encode terms modulo alpha-conversion for a wide range of
object languages in a straightforward fashion.  The design of FML is
`semantically driven', in that it arises from the model of variable
binding in terms of Fraenkel-Mostowski sets given by the authors in
(Gabbay and Pitts 1999).  Compared with Standard ML (Milner, Tofte,
Harper, and MacQueen 1997), the language has a novel type constructor
for abstractions; facilities for declaring locally fresh names; and
recursive definitions can use a form of pattern-matching on bound
names in abstractions. The crucial point is that the FML type system
ensures that these features can only be used in well-typed programs in
ways which are insensitive to renaming of bound names.