Abstract Syntax and Variable Binding


       Marcelo Fiore             Gordon Plotkin            Daniele Turi
           COGS                       LFCS                     LFCS
      Univ. of Sussex          Univ. of Edinburgh       Univ. of Edinburgh
  <marcelo@cogs.susx.ac.uk>    <gdp@dcs.ed.ac.uk>        <dt@dcs.ed.ac.uk>



                                    Abstract

  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 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.