Paper: Abstract Syntax and Variable Binding (at LICS 1999)
Authors: Marcelo Fiore Gordon Plotkin Daniele TuriAbstract
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.
BibTeX
@InProceedings{FiorePlotkinTuri-AbstractSyntaxandVa, author = {Marcelo Fiore and Gordon Plotkin and Daniele Turi}, title = {Abstract Syntax and Variable Binding}, booktitle = {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999}, year = 1999, editor = {Giuseppe Longo}, month = {July}, pages = {193--202}, location = {Trento, Italy}, publisher = {IEEE Computer Society Press} }