By Marcelo P. Fiore, Gordon Plotkin and Daniele Turi, from LICS 1999, available from the Edinburgh Research Archive website:
We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. 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.