Concurrent Structures in Game Semantics
Castellan, Simon · Spiral (Imperial College London) · 2017
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.