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

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