Abstract Syntax and Variable Binding (Extended Abstract)
Marcelo Fiore, Gordon D. Plotkin, Daniele Turi · ERA · 2003
Abstract 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 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.