I will present joint work with Francois Maurel, streaming from both Girard's Ludics and the recent work in Game Semantics aiming to model concurrent forms of interaction.
We introduce abstract structures corresponding to proofs/programs, strategies in Games Semantics and designs in Ludics. Our structures are graphs rather than trees, and interactions (plays) result into partial orders rather than linear sequences.
Syntactically, this corresponds to working with abstract proof-nets, rather than with abstract sequent calculus derivations (in MALL: multiplicative-additive linear logic). The switch to proof-nets allows for parallelism and multi-focalization.