Game Semantics

Prerequisites

Students are expected to have strong mathematical ability and be familiar with basic dis­ crete mathematics (sets, functions, relations, order relations, first­order logic). The course would make a good combination with Lambda Calculus or Domain Theory or Program­ ming Languages or Concurrency, but does not assume any material taught in these courses as a prerequisite.

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 (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 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.