Andy Pitts

This talk describes an approach to formalising certain notions that

are common in the practice of representing and reasoning about syntax

involving variable binding. I concentrate on the use of explicitly

named bound variables, rather than on the use of nameless terms, or

higher order abstract syntax. Nominal Logic, a version of first order

many sorted logic, gives a mathematical status to the taxonomic

distinction often made between free and bound names. It contains

primitives for renaming via name-swapping and for freshness of

names. Its axioms express key properties of these primitives derived

from the FM-sets model of syntax introduced by Gabbay and Pitts. The

main point of the talk is to emphasise the usefulness, for the

practice of operational semantics, of making explicit the equivariance

property of assertions about syntax---namely that their validity is

invariant under swapping bindable names.

Paper available at: www.cl.cam.ac.uk/users/amp12/papers/index.html#nomlfo