@InProceedings{PittsAM:newaas,
author = {M.~J.~Gabbay and A.~M.~Pitts},
title = {A New Approach to Abstract Syntax Involving Binders},
booktitle = {14th Annual Symposium on Logic in Computer Science},
year = 1999,
publisher = {IEEE Computer Society Press, Washington},
pages = {214--224},
abstract = {The Fraenkel-Mostowski permutation model of set theory with atoms
(\emph{FM-sets}) can serve as the semantic basis of meta-logics for
specifying and reasoning about formal systems involving name
binding, $\alpha$-conversion, capture avoiding substitution, and so
on. We show that in FM-set theory one can express statements
quantifying over `fresh' names and we use this to give a novel
set-theoretic interpretation of name abstraction. Inductively
defined FM-sets involving this name-abstraction set former (together
with cartesian product and disjoint union) can correctly encode
object-level syntax modulo $\alpha$-conversion. In this way, the
standard theory of algebraic data types can be extended to encompass
signatures involving binding operators. In particular, there is an
associated notion of structural recursion for defining
syntax-manipulating functions (such as capture avoiding
substitution, set of free variables, etc) and a notion of
proof by structural induction, both of which remain pleasingly close
to informal practice.}
}