An EPSRC funded research project based at:


Nominal sets provide a promising new mathematical analysis of names and binding. This project will investigate whether this new piece of mathematics can give rise to better computer systems for formalising programming language semantics and developing programs certified against the semantics, in which the issues of names and binding are treated in a more expressive and user-friendly fashion than at present. The FreshML project in Cambridge has investigated this in the context of functional programming. We will extend this existing work in a new direction, by developing the equational logic of nominal sets, nominal term-rewriting, and associated algorithms (for unification, matching, residuation, narrowing, etc.) We aim to producing functional logic programming languages and machine-assisted theorem provers supporting a form of structural recursion/induction modulo alpha-equivalence that remains faithful to informal practice.