Game semantics using function inventories

This talk presents work in progress. We analyze the semantics of
higher-order references presented by Abramsky, Honda and McCusker, and
see that a term's denotation can be obtained directly from operational
semantics. (By contrast with earlier work, it is not necessary for the
term to be eta-long.) The principle is that players pass each other
functions, so that each player's inventory of functions grows over
time. This gives a convenient operational technique for proving
observational equivalence. It also give an account of the denotational
semantics using the set of strategies is given by a domain equation,
and pointers between moves are no longer required. And there are
variant domain equations for the various constraints (bracketing,
visibility, innocence) that may be imposed.

This is joint work with Soren Lassen.