Lecturer	Andrzej Murawski
Class Tutor	Nikos Tzevelekos

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.

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

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.