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.

Available as:


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.

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

Daniele Turi
Last modified: Mon Jun 25 15:25:45 BST 2001