Notes for research students

There isn't very much here right now, but hopefully the collection will grow over time. I would be delighted to receive feedback on any of the items below. That would allow me to revise these notes.

Introduction to Games used for Semantics. These can be viewed as an attempt to supply some of what's only being sketched out in Martin Hyland's Game Semantics. The category of `simple games' is described here, and we sketch how this can supplies a model of linear logic. No attempt is made to explain innocence, or related notions. These notes are suitable for readers who have had some exposure to category theory but don't know much about games. A handful of people have told me they found it useful, but I haven't had any further feedback on it. I suspect there are some minor errors at least. There is also a pdf version.

Some notes on monads. This is a short introduction to monads. It motivates the definition, makes the connection to Kleisli triples and then proceeds to explain the Kleisli category and the category of Eilenberg Moore algebras for a monad. It assumes that the reader is familiar with category theory up to adjunctions.

What is a categorical model of linear logic?. This is an introduction to what it means to be categorical model of linear logic. While it tries not to assume more than the definition of adjunction, it gets somewhat dense when it comes to giving the interpretation of the linear exponentials. Not all diagrams are given explicitly. However, a characterization for such a model is given which did not not seem to be present in the literature when I wrote these. Now largely superceded by Paul-Andre Mellies' chapter Categorical semantics of linear logic in `Interactive models of computation and program behaviour'.

Together with Martin Hyland I've written a paper on the (double) glueing technique, and how it can be used to build more sophisticated models of linear logic from simple ones. This includes a description of using a notion of orthogonality to identify subcategories with an even more sophisticated structure. This paper may be hard to read for research students, and so I've written a gentler introduction by concentrating on the special case of glueing a long hom-functors, which is also available as a pdf file.

On a rather different topic, one of my third year project students has given an algorithm that takes a program in the While language and turns it into a PCF term, together with a proof that the meanings of the two agree in an appropriate sense. This is an interesting idea and requires matching the fixed point constructions underlying the two models. My notes explaining this are available here.


There are various notes written by Harold Simmons some of which I've based some of my teaching on.
9 August 2012