Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Logic and Semantics Seminar
24th October, 1997: Guy McCusker
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 24th October, 1997: Guy McCusker

Speaker: Guy McCusker, University of Oxford
Title: Games, Factorizations, Definability and ML-Style References
Time: 24th October, 1997, 14:00
Abstract:

A few years ago, game semantics came to the fore when it was used to provide fully abstract models of the functional langauge PCF (see the work of Hyland, Ong, Nickau, Abramsky, Jagadeesan and Malacaria). Such models interpret PCF programs as strategies for certain games; various behavioural conditions are imposed on these strategies which guarantee that every "good" strategy corresponds to a program, yielding a definability result which leads to full abstraction.

Since that pioneering work, a programme of research has emerged which seeks to capture in the same precise fashion the behaviour of languages more complex than PCF, such as languages with store, or with control operators. Somewhat surprisingly, a uniform picture is building up which associates each of the behavioural conditions imposed on the strategies with the existence of a particular programming language feature: relaxing a condition on the model of PCF allows one to obtain a model of an extended language. Factorization results which connect the relaxed models with the highly constrained model of PCF are then used to lift PCF definability to the extended languages.

This talk will present an overview of the results obtained so far, and go on to show how the relaxation of a further condition allows higher-order store, like the references of Standard ML, to be modelled, and a full abstraction result to be obtained. These new results are the product of joint work with Samson Abramsky and Kohei Honda.