Nominal Semantics of Abstraction and Restriction

Many uses of names in programming languages and logical calculi are "atomic", in the sense that the structure of a name is immaterial: all that matters are distinctions between names and the association of names to the things named. In this talk I will give a gentle introduction to the topos of "nominal sets", a mathematical framework with names as atoms that can express the crucial property of "freshness" of names in a syntax-independent way. There are simple constructions on nominal sets for exponentiation, for name-abstraction and for name-restriction that illuminate the relationship between these notions and that of dynamic allocation of names in operational semantics. The category-theoretic characterisation and properties of name-abstraction and name-restriction hint at a categorical algebra for "equations modulo freshness constraints" that has yet to be investigated.
Last modified: Fri Aug 6 09:38:22 BST 2004