Equivariant and Nominal SOS (Abstract)

Many kinds of names 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. One says that a semantic construct involving such atomic names is "equivariant" if its meaning is preserved under the operation of permuting the atoms. A simple, but useful, result about finitary inductive definitions shows that equivariant relations already abound for structural operational semantics carried out in ordinary (naive) set theory. However, to really exploit the power of this permutation-oriented viewpoint for general inductive and co-inductive definitions (such as occur in concurrency theory) and for modelling locality and abstraction of names, requires a modest change of foundation to "nominal sets". This is a mathematical framework with names as atoms that makes equivariance ubiquitous and can express the crucial property of "freshness" of names in a syntax-independent way.

Last modified: Tue Aug 31 09:54:04 BST 2004