Interaction between two or more agents, subject to predetermined rules, may be represented as a formal game. This rather natural idea crops up repeatedly: games are used and studied in various branches of mathematics, logic, economics and computer science (game theory, Ehrenfeucht-Fra´ssÚ games, model-checking games...) although the connections in many cases are rather superficial.

I am principally interested in game semantics , in which a program is interpreted as a strategy for one participant in a two-player game, representing a program type or specification. Consistent with the "Curry-Howard" correspondence winning strategies may also represent proofs in a game representing a logical formula. The main difference to other mathematical and logical games is that we are not just interested in whether there is a strategy for a given game, or whether one strategy is "better" than another (although these are important questions), but how strategies interact together, representing computation or proof-normalization.

Because they represent interaction between programs and the environment directly, games models generally give more information about the behaviour of programs than traditional denotational semantics. By constraining strategies appropriately, we can give interpretations with formal properties such as full abstraction. Ongoing research is also concerned with using them to establish important properties of programs such as safety, security, and bounded resource usage.

My research

My research in game semantics has been focussed on giving denotational models of functional programming languages and calculi with other features or side-effects, such as non-local control (including continuations, exceptions and coroutines), state (integer and general references), including local names and pointers, and concurrency (the pi-calculus and higher-order message-passing). I have studied various properties of such models, such as decidability of contextual equivalence or the theory underlying them (for example category theoretic presentations, or their relationship with continuation-passing interpretation and other operational theories such as labelled transition systems.


Games for Logic and Programming (Galop) is a series of workshops focussed on game semantics.