14/10/2002
Jamie Gabbay (Univ. of Cambridge)
Fraenkel-Mostowski (FM) techniques for syntax with binding

It is well-known that inductive definitions can interact poorly with variable binding. As a simple example, in defining capture-avoiding substitution we may have to rename bound variables and there is no canonical way of doing so. Difficulties include

• coding algorithms in optimising program transformations,
• formal analysis of syntax (for example, using operational techniques to analyse program equivalence),
• verifying bisimulation equivalence in process calculi with binding, such as the pi-calculus,
• logics for describing syntax-with-binding,
• writing parsers, pretty-printers, interpreters, compilers, and any other program which manipulates syntax-with-binders.

FM (Fraenkel-Mostowski) techniques give a semantics to binding based on a novel mathematical foundation. I claim that this foundation provides an explanation of binding from first principles, and that this account is a mathematically beautiful one. We use this semantics to develop novel and improved logics and programming languages.

Thus I shall talk about FM semantics in general and then show examples of the programming languages and logics which emerge from it.

I am employed on the FreshML project in the Cambridge Computer Laboratory, UK. We are implementing an ML-style language which includes features for declaring inductive datatypes of syntax with binding, designed using soundness with respect to an FM semantics.