Lectures on Nominal Syntax and Semantics
International Summer School on Applied Semantics,
Fauenchiemsee, Germany, 812 September, 2005
Formal languages involving names and constructs that bind names abound
in computer science. Much effort has been expended to find
mathematical theories of "syntax modulo renaming bound names" that
have good logical and computational properties, but are also easy to
use. These lectures introduce the theory and applications of "nominal
sets", a new mathematical model of names and binding based on simple,
but subtle ideas to do with permutations of names that first arose in
mathematical logic in the 1930s. At the heart of the approach is the
notion of "finitely supported" mathematical objects. The lectures
will explain the idea in as concrete a way as possible and will
discuss its consequences for programming language semantics and for
the design of functional and logical metaprogramming languages.
