Skip to main content

Game Semantics

Game semantics is a versatile modelling approach that views computation as an exchange of moves between two players, representing respectively the program and the context in which the program is executed. The pioneers of the subject (Abramsky, Jagadeesan, Malacaria, Hyland, Ong, Nickau), three of whom were in Oxford at the time, received the 2017 Alonzo Church Award for Outstanding Contributions to Logic and Computation.

Game semantics makes it possible to construct very faithful models of programming languages, called fully abstract in technical parlance. In the last three decades, such models have been constructed for a whole spectrum of programming languages, ranging from purely functional ones to languages with rich feature sets such as higher-order references, exceptions and objects.

Current research in the area focusses on tackling emergent programming paradigms and exploiting the accuracy and compositionality of game-semantic modelling to attack problems in program verification, notably program equivalence. The more applied strand of work often capitalizes on unexpected connections between game models and other areas, such as automata, category theory and operational semantics, with a view to extending existing verification techniques in novel ways.

 

Faculty

Students