abstract syntax and variable binding

The preprint

	Abstract Syntax and Variable Binding 


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

is available as



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.