Summer School on Game Semantics

22-26 August 2016


Instructor: Dan Ghica, University of Birmingham, UK.

General Information

The school will be carried out in English, attendance is free of charge, but the number of participants is potentially limited. The exact time and venue will be announced later. The school is aimed at senior bachelor and master students, post-graduates, researchers and developers, interested in novel research topics in computer science and programming languages.

To register for the school and receive future announces please join the following group:!forum/jbr_summer_school_on_game_semantics


Game Semantics is a method of modelling programming languages based on the way terms interact with their context. Game Semantics is usually expressed denotationally (i.e. inductively on the abstract syntax of the language) and leads to models with a very high level of mathematical precision (“fully abstract”). This technique came to prominence when it gave the first definability result for PCF, but it went on to provide models for an incredibly broad range of programming languages combining higher-order functions and effects, such as local state, non-determinism, concurrency, polymorphism, control and combinations thereof. It is fair to say no other style of denotational semantics comes close in modelling power and accuracy. Moreover, the elementary and algorithmic nature of game semantics made it suitable for highly innovative applications to automated program verification, and to compilation for unconventional platforms. The syllabus of the course is:

  1. Preliminaries: abstract-machine programming language semantics, nominal sets
  2. System level semantics: an operational approach to modelling open terms
  3. Game semantics: a denotational model of polarised traces
  4. Applications to automatic verification
  5. Applications to high-level synthesis
  6. Applications to distributed compilation
  7. Related topics: Geometry of Interaction, trace semantics
  8. Research topics