Concurrent Games is a framework developed in the past decade for semantics of programming languages. In Concurrent Games, a program is interpreted as an event structure, representing its interactive behaviour with its execution environment. The representation is extremely fine-grained: it is causal as in so-called truly concurrent models of concurrency, showing explicitely the dependence and independence of computational events, and the non-deterministic branching points.

This interpretation is computed in a modular way by induction on programs, following the methodology of denotational semantics. This is good, because it means that the semantics can be used to reason compositionally on programs. But it is also bad, because the many layers of the interpretation of the source code in a denotational model and the complexity of the operations involved (notably, the composition of strategies) blurs the relationship between the source code and the semantics.

In this work, we make concurrent games operational. More precisely, we show that programs can be translated compositionally intro certain coloured Petri nets, combining intuitions from game semantics, Girard's Geometry of Interaction, and folklore ideas on the representation of first-order imperative concurrent programs as Petri nets. We regard these coloured Petri nets as a kind of intermediate representation, still close to the source code. But as finite graphs unfold to infinite trees, Petri nets unfold to event structures; and here we show that this unfolding yields the same event structure obtained denotationally from the interpretation in concurrent games.

We deploy this for Idealized Parallel Algol, a call-by-name higher-order concurrent programming language that is well-studied in the game semantics literature. The translation is implemented, and available at:

https://ipatopetrinets.github.io/

This is joint work with Simon Castellan.