Game Semantics: 20072008
Lecturer 

Class Tutor 
Overview
Game 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 (lowlevel 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 computeraided program verification and, time permitting, we shall touch upon this topic towards the end of course.Learning outcomes
On 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.Prerequisites
Students 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.Synopsis
 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
Reading list
 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