# abstract syntax and variable binding

The preprint

Abstract Syntax and Variable Binding

by

M. Fiore, G. Plotkin, and D. Turi

is available as

http://www.dcs.ed.ac.uk/~dt/abstractsyn.ps

Synopsis:

We develop a theory of abstract syntax with variable binding.
To every binding signature we associate a category of models
consisting of \emph{variable sets} endowed with both a (binding)
algebra and a substitution structure compatible with each other.
The syntax generated by the signature is the initial model.
This gives a notion of initial algebra semantics encompassing
the traditional one; besides compositionality, it automatically
verifies the semantic substitution lemma.