Title: 

Algebraic theories in the presence of binding operators, substitution,
etc.

Abstract:

Binding algebras [1] provide an algebraic model for first-order syntax
with variable binding that provides an initial-algebra semantics
encompassing substitution as an algebraic operation.  The generality
in which one would wish to incorporate equations in this and related
settings, however, does not straightforwardly fit into the typical
approach to equational theories, eg. [2].  For instance, the
specification of the beta and eta equations in the untyped lambda
calculus requires operators with types involving a mixture of
cartesian products and substitution tensors. To tackle this problem,
we revisit the notion of equational theory in a new, more abstract but
simpler, light way.  The resulting theory supports free constructions,
etc. and is directly applicable to algebraic theories with binding
operators, substitution, etc.

I will present this talk with concrete examples such as groups and the
untyped lambda-calculus. Only basic category theory (functors, natural
transformations, limits) will be assumed.

This is joint work with Marcelo Fiore.

[1] M.Fiore, G.Plotkin and D.Turi.  Abstract syntax and variable
binding.  In LICS'99, 1999.

[2] G.M.Kelly and J.Power.  Adjunctions whose counits are coequalizers
and presentations of finitary enriched monads.  JPAA, 1993.