Nominal Logic:  A First Order Theory of Names and Binding

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: