  Formalizing syntactic proofs of properties of logics, programming languages,
security protocols, and other formal systems is a significant challenge, in
large part because of the obligation to handle name-binding correctly. We
present an approach called nominal abstract syntax that has attracted
considerable interest since its introduction approximately six years ago. After
an overview of other approaches, we describe nominal abstract syntax and
nominal logic, a logic for reasoning about nominal abstract syntax. We also
discuss applications of nominal techniques to programming, automated reasoning,
and identify some future directions.
