Game Semantics: 2007-2008
OverviewGame Semantics is a relatively new framework for describing the meaning of programs. It views computation as an exchange of moves between two players and interprets programs as strategies for one of them. Remarkably, various features of programming languages, such as state and control, can be related to combinatorial conditions regarding plays and strategies. This results in very accurate models that satisfy a technical condition called full abstraction (a kind of holy grail in programming language semantics). This course will provide an introduction to the semantics of programming languages and game semantics in particular. We shall discuss desirable correspondences between abstract mathematical semantics and operational semantics (low-level execution semantics), and introduce standard techniques for proving them. Prototype programming languages will be defined to demonstrate a variety of programming language features in their pure form and, for each of them, we shall construct fully abstract game models. The insights from game semantics have recently been applied to computer-aided program verification and, time permitting, we shall touch upon this topic towards the end of course.
Learning outcomesOn completion students will understand the goals of programming languages semantics. Given a program, they will be able to explain the process of constructing a corresponding strategy, and, conversely, given a strategy of a suitable kind, they will be able to synthesize a corresponding program. They will understand the notion of full abstraction and be able to prove that the game models introduced in the course are fully abstract.
PrerequisitesStudents are expected to have strong mathematical ability and be familiar with basic discrete mathematics (sets, functions, relations, order relations, first order logic). The course would make a good combination with Lambda Calculus or Domain Theory or Programming Languages or Concurrency, but does not assume any material taught in these courses as a prerequisite.
- Games in computer science
- Types and programs, structural operational semantics
- PCF as a prototypical functional programming language
- Idealized Algol as a synthesis of functional and imperative programming
- Control primitives
- The playground: arenas and plays
- Strategies and compositionality
- Computational soundness and adequacy
- Decomposition techniques
- Definability and full abstraction
- Algorithmic game semantics
- S. Abramsky, G. McCusker: Game semantics
- R. Harmer: Games and full abstraction for nondeterministic languages
- J. M. E. Hyland, C. – H. L. Ong: Full abstraction for PCF