Game Semantics and its Applications

Abramsky, Ong and their collaborators pioneered the development of game semantics in the 1990s and, during the assessment period, investigated many applications to programming languages and the semantics of logical proof. This research has now taken a major algorithmic turn, with striking applications to compositional model-checking and program analysis. We pioneered the use of games to characterise the complexity of program equivalence for certain classes of higher-order programming languages. Recently, a powerful combination of game semantic methods, automata and complexity theory, and verification techniques has led to exciting new results on decidability and complexity of verifying properties of infinite-state and probabilistic systems. Game semantics is now one of the liveliest approaches in the semantics of computation, and Oxford is a major centre. Several notable achievements have flowed from Abramsky and Ong's £300K EPSRC project on Algorithmic Game Semantics. Key results include a game semantics for generic polymorphism, solving a problem open for some 10 years. Murawski won the ETAPS'05 best theoretical paper award, and was elected to a Research Fellowship at St John's College as well as an EPSRC Advanced Fellowship. Nikos Tzevelekos won the Kleene Best Student Paper award at LICS'07 for his work on Full Abstraction for Nominal General References. A £430K EPSRC Platform Grant was secured to support new developments within the Centre for Metacomputation.