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