University of Cambridge

Logic
&
Semantics

A Metalanguage for Programming with Bound Names Modulo Renaming

By Andrew Pitts (8th October 1999)

This talk will describe work in progress (with Jamie Gabbay) on the design of an ML-style metalanguage, FML, for programming recursively defined functions on user-defined datatypes whose constructors may involve binding. Object language terms modulo alpha-conversion can be faithfully represented up to operational equivalence as values of suitable FML datatypes. The design of FML is `semantically driven', in as much as it arises out of contemplating the model of variable-binding in terms of Fraenkel-Mostowski sets given in [Gabbay and Pitts, Proc. LICS '99, pp 214--224]. Compared with ML, the language has a novel type constructor for abstractions; facilities for declaring fresh names; and recursive definitions can use a form of pattern-matching on bound names of 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.

LS Home page or Talks in 1999/2000