Abstract Syntax and Variable Binding

Syntax and Variable Binding d Abstract) Marcelo Fiore COGS Univ. of Sussex Gordon Plotkin LFCS Univ. of Edinburgh Daniele Turi LFCS Univ. of Edinburgh op 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.

• Type: Conference
• Year: 1999
• Where: LICS
• Authors: Marcelo P. Fiore, Gordon D. Plotkin, Daniele Turi
• Keywords: Automated Reasoning, LFCS Univ, LICS 1999, Turi LFCS Univ, Variable Binding