Concurrent Structures in Game Semantics

Abstract

Game semantics is a powerful tool to design intensional denotational
semantics of complex programming languages, leading to notions of syntaxfree
normal forms and fully abstract models. In game semantics, programs
become strategies, ie. set of plays, on a game given by their type.
Traditionally, game semantics represents plays as sequences of moves.
This representation forces to reduce concurrency to interleavings. In this
paper, we develop a framework of game semantics based on event structures
– a partial order representation of concurrency, extending the work of
Rideau and Winskel [19]. This causal representation allows to retain more
intensional behaviour on concurrent programs. We demonstrate the benefits
of this approach by developing a notion of concurrent and nondeterministic
innocence, which an open problem despite the existence of many game semantics
models of concurrent languages. We show that, our innocence along
with an extension of well-bracketing, can capture the essence of parallel and
nondeterministic computation.