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