Abstract Syntax and Variable Binding

Marcelo Fiore, Gordon Plotkin, and Daniele Turi

In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, LICS '99, pages 193--202. IEEE Computer Society Press, 1999.

• (216K) PDF
• (184K) Postscript

Abstract

We develop a theory of abstract syntax with variable binding. We associate to every binding signature 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.

@InProceedings{FiorePlotkinTuri99,
	author = {Marcelo Fiore and Gordon Plotkin and Daniele Turi},
	title = {Abstract Syntax and Variable Binding
		  (Extended Abstract)},
        Organization={IEEE},
        Publisher={Computer Society Press},
        Booktitle={Proc.\ 14$^{\rm th}$ LICS Conf.},
        pages = {193-202},
	year = {1999}
}