Andrew Pitts
University of
Cambridge Computer Laboratory
Abstract:
Many kinds of names (or identifiers) occurring 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. The main point of this
talk is to emphasize the usefulness of taking into account the
"equivariance property" of semantics---namely that meaning is invariant
under permuting such names. We give a gentle introduction to "nominal
sets", a mathematical framework with names as atoms, which makes
equivariance ubiquitous and can express the crucial property of
"freshness" of names in a syntax-independent way. There are simple
constructions on nominal sets for functions, for name-abstraction and
for name-restriction that illuminate the relationship between these
notions and that of dynamic allocation of names in operational
semantics.
Host: Frank Pfenning
Appointments: Jennifer
Landefeld
Principles
of Programming Seminars
Monday, June 28, 2004
3:30 p.m.
Wean Hall 4623