# Abstract Syntax and Variable Binding

## Marcelo Fiore, Gordon Plotkin, and Daniele Turi

Available as:

### 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}
}


Daniele Turi