Nominal techniques: a success story of the continued relevance of mathematical foundations to computer science

Jamie Gabbay (Heriot Watt)

Wednesday 23rd March, 2011 16:00-17:00 204

Abstract

In the 1930s Fraenkel and Mostowski designed a set theory that bears their name and used it to prove the independence of the axiom of choice from the other axioms of set theory. In 1999 I and Pitts rediscovered this model and used it to model syntax trees with binding. Although initially perceived as a technical "trick" for making certain things work in mechanised mathematics, I believe that we had accidentally stumbled upon a whole new foundation for logic and programming.
Of course, that foundation was not actually new; it had been exploited in set theory, and permutations of first-order structures are well-studied field. But some important extra bits were added to this story, and the connection with applications in computer science, is new.
What distinguishes "nominal" foundations is an assumption of a collection of names (or atoms or urelemente) which are symmetric under the group of permutations of names, and which have a finite support property (which is exactly the same as that property used in the set-theoretic independence proofs).
In this talk l will try to describe---in broad terms aimed at the non-specialist---why these symmetries are so useful, and how we can exploit them to develop new classes of logics and models. I will describe why working with groups of permutations can be preferable to working with monoids of renamings, and why taking names as primitive can be so useful when we already have plenty of other sets available (such as numbers). I will sketch the overall use of first-order axiomatisation in computer science, and locate within that the planned application of nominal techniques.
The interested reader can find material on this on on my webpage and in particular can look at two recent survey articles on nominal logics and on foundations.

Add to your calendar

Download event information as iCalendar file (only this event)