Asynchronous games: the concurrent geometry of proofs

Game semantics has taught us the art of transforming proofs into
interactive strategies. These strategies are generally defined in a
purely sequential way, as a set of alternating sequences (= plays)
exploring the branch of a decision tree. This is reminiscent of
interleaving semantics in concurrency theory, where a process
generates a set of sequences (= traces).
Asynchronous games are played on event structures, rather than trees.
Shifting to asynchronous games enables to extract the truly concurrent
semantics of proofs from their interleaving semantics, by identifying
plays modulo permutation of moves --- understood geometrically as an
homotopy relation in the n-dimensional space generated by the event
structure.
The truly concurrent nature of innocence in arena games is captured by
a pair of diagrammatic properties (forward and backward innocence)
formulated in asynchronous games. The analysis reveals that innocent
strategies are *positional* in the game-theoretic sense that they play
according to their current position. Positionality together with a
*payoff* or a *truth value* on positions leads unexpectedly to an
innocent game model of propositional linear logic --- with the usual
well-bracketed and non well-bracketed models as intuitionistic
fragments, and a structure-preserving functor to the relational model.