An EPSRC funded research project
based at:
Summary
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.