Categories, Proofs and Games

Overview

A fundamental way of understanding computation is in terms of interaction between a system and its environment: for example, a program component (e.g. a function, procedure or object), and the context in which it is evaluated; or a concurrent process, and the larger system in which that process runs. We can also view logic in these terms, so that a formula is understood in terms of the possible interactions between a `Proponent' of the thesis or assertion expressed by the formula, and an "Opponent", who seeks to refute it.

This perspective on computation and logic can be made precise using ideas from game theory, and leads to a mathematically rich and fruitful approach which has already led to a number of interesting applications.

In this course we shall introduce the basic ideas of game semantics, together with some necessary background in elementary category theory and proof theory, and show how these ideas can be applied to modelling and reasoning about programming languages.