LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4pm, Tuesday 18th November 1997

Title: Games, factorizations, definability and ML-style references

Speaker: Guy McCusker (St John's College, Oxford)

A few years ago, game semantics came to the fore when it was used to provide fully abstract models of the functional language 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.