Game Semantics, a reading course

Wednesdays at 3.15 pm in room S2 (1304) beginning 25 November.

Game semantics and linear logic are two related fields of research which try to get to the heart of the nature of computation.

Game models have recently become popular after the constructions of fully abstract models of PCF by Abramsky, Jagadeesan and Malacaria, and by Hyland and Ong. They have also been used to give semantics of classical logic, and are studied with the aim of extracting computational content from proofs in classical logic.

Linear logic was invented by Girard in the mid 80-ies. It attracted much attention since it aimed to give rise to "resource-conscious" functional programming and perhaps also to a logically based process calculus.

For further information, contact the course leader, Peter Dybjer.

Currently planned presentations:

25 November: Introduction to Linear Logic, Peter Dybjer
2 December: Game Semantics: an Informal Introduction (section 1-2 from Abramsky and McCusker [1]), Henrik Persson
9 December: Categories of Games (section 3 from [1]), Makoto Takeyama
16 December: Game Semantics of PCF (section 4 from [1]), Koen Claessen
?? January: Classical Sequent Calculus, Qiao Haiyan
?? January: Game Semantics of Classical Logic, Thierry Coquand

Suggested future topics

week 6, 1999: Games and State ([1] section 5)
week 7, 1999: Games and Control ([1] section 6)

We will be using the following survey papers:

[1] Game Semantics (lecture notes from the 1997 Marktoberdorf Summer School), Samson Abramsky and Guy McCusker. Available from Guy McCusker's home page.
[2] Computational Content of Classical Logic (lecture notes from the Semantics of Computation Summer School at the Newton Institute 1995), Thierry Coquand, available from Thierry Coquand's home page.

Some other interesting papers on games:

Game Semantics (lecture notes from the Semantics of Computation Summer School at the Newton Institute 1995), Martin Hyland.
The mother of all closure operations, draft paper by Peter Hancock containing ideas how to define games inside type theory.
Free Lattices, Communication and Money Games, Andre Joyal.
On the Meaning of the Logical Rules I: Syntax vs. Semantics, Jean-Yves Girard.

There is also interesting material discussing games, sequentiality and the full-abstraction problem, games and abstract machines, games and call-by-value/call-by-name, etc. See e.g. Kohei Honda's homepage

Some interesting papers on linear logic:

The linear abstract machine, Yves Lafont.
A linear functional language, draft paper by Soren Holmstrom.
Computational interpretation of linear logic, by Samson Abramsky.
Linear types can change the world! and other papers on linear logic by Phil Wadler

Please contact the course leader if you want a copy of a paper that is not available via the web.

Last modified: Tue Dec 8 16:36:56 MET 1998