Abstract Syntax and Variable Binding (Extended Abstract)
View/ Open
Date
06/11/2003Author
Fiore, Marcelo P
Plotkin, Gordon
Turi, Daniele
Metadata
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
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 veri-
fies the semantic substitution lemma.