Marcelo is visiting Edinburgh for the next six weeks (office 2412).

Abstract

Universal algebra is a robust mathematical theory for the study of equational theories. It is based on semantic considerations involving models (algebras) and their homomorphisms. An important role in the theory is played by free constructions in general and by initial algebras in particular. For instance, as it is well-known, the initial algebra over a signature provides an abstract description of the syntax generated by the signature. Moreover, the universal property given by initiality endows the initial algebra with an induction proof principle to reason about it, and the unique algebra homomorphism amounts to a definition by structural (or primitive) recursion which may be used to define useful operations as, for example, substitution. Thus, the theory may be also used for syntactic purposes.

Our long term research aim is to extend the above theory to encompass higher-order operators. In this talk, as a step towards this direction, I will focus on the afore-mentioned syntactic aspects of such an extension. In particular, I will show how higher-order syntax (viz. syntax with binding operators) can be seen as an initial algebra and discuss the issue of defining substitution. As further work we hope to use this semantic framework to aid the design of a type theory for specifying and reasoning about higher-order syntax.

This is work in progress in collaboration with Gordon Plotkin and Daniele Turi.