[Prev][Next][Index][Thread]
A meta language for programming with bound names
The following preprint is available electronically via:
<http://www.cl.cam.ac.uk/users/amp12/papers/index.html#metlpb>
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
Abstract
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.
----------------------------------------------------------------------