<figure><img src="image_240.png" /><figcaption>Figure 13.8: Composition of $\sigma$ and $\tau$</figcaption></figure>

on the choice of the mediating symmetry $\theta_B$ – which in hindsight should have been
obvious with some familiarity with the resource calculus, because $\theta_B$ somehow corre-
sponds to the non-determinism of reduction in the resource calculus (see Section 13.4).
As a matter of fact, (13.2) fails; let us see a counter-example:

**Example 13.3.1.** Take the board $\alpha$ with one event $\mathbf{q}^{-}$, $\kappa_{\alpha}(\emptyset) = 1$, $\kappa_{\alpha}(\{\mathbf{q}^{-}\}) = 0$, and

$$
\sigma : !\left(\alpha \to \alpha\right) \vdash !\alpha \to \alpha, \qquad \tau : !\left(\alpha \to \alpha\right)
$$

two strategies as in Figure 13.8. Their assignment of copy indices uses functions

$$
f : \mathbb{N} \to \mathbb{N}, \quad g : \mathbb{N} \to \mathbb{N}, \quad h : \mathbb{N} \to \mathbb{N}, \quad k : \mathbb{N}^2 \to \mathbb{N},
$$

whose precise identity is irrelevant. Their composition unfolds as in Figure 13.8, yielding four pairwise conflicting, non-symmetric positive moves.

Enriching non-deterministic PCF with a type $\alpha$ with no constant, the substitution

$$
(\lambda x^{\alpha}. f (f x)) [(\lambda y^{\alpha}. y \otimes y) / f]
$$

gives a perfect syntactic counterpart to the composition in Figure 13.8. As there are
two calls to the non-deterministic choice, this reduces to $\lambda x^\alpha . x$, but in four different
ways. In the copy indices of each positive move of $\tau \odot \sigma$, one can read back how the
two non-deterministic choices were resolved: the upper row corresponds to the first call
yielding $\mathbf{q}_{i,f(i)}^+$, the leftmost column to the second call yielding $\mathbf{q}_{\tau,f(i)}^+$, and so on.

Reading back witnesses from the components and their composition, we have

$$
\#\mathrm{wit}_{\tau \odot \sigma} \left( \begin{smallmatrix} \mathbf{q}^{-} \\ \mathbf{q}^{+} \end{smallmatrix} \right) = 4, \quad \#\mathrm{wit}_{\sigma} \left( \begin{smallmatrix} \mathbf{q}^{-} & \mathbf{q}^{-} & \mathbf{q}^{-} \\ \mathbf{q}^{+} & \mathbf{q}^{+} & \mathbf{q}^{+} \end{smallmatrix}, \begin{smallmatrix} \mathbf{q}^{-} \\ \mathbf{q}^{+} \end{smallmatrix} \right) = 1, \quad \#\mathrm{wit}_{\tau} \left( \begin{smallmatrix} \mathbf{q}^{-} & \mathbf{q}^{-} \\ \mathbf{q}^{+} & \mathbf{q}^{+} \end{smallmatrix} \right) = 3;
$$

as $\sigma$ and $\tau$ cannot synchronize on any other symmetry class, this contradicts (13.2).

After staring at this example for a while, it seemed that the mistake was in the enumer-
ation of the witnesses for $\tau$. Indeed, up to symmetry, there are exactly three configura-
tions of $\tau$ corresponding to two calls: (1) both choices may be resolved with $\mathbf{q}_{i,f(i)}$ (call
this “left-left”); (2) both choices may be resolved with $\mathbf{q}_{i,g(i)}$ (call this “right-right”);
and (3) we may have one of each. But arguably, (3) really identifies two cases: (3a) “left-right” and (3b) “right-left”. Those configurations are symmetric, but it turns out that **TCG** is equipped with exactly the right tool to keep them distinct. Imagine fixed, for every $x_A \in (A)$, a concrete representative $\underline{x}_A \in x_A$. Then, for $\sigma : A$ we set

$$ \mathrm{wit}_{\sigma}^{+}(x_A) = \{x^{\sigma} \in \mathscr{C}^{+}(\sigma) \mid \partial_{\sigma} x^{\sigma} \cong_{A}^{+} \underline{x}_{A}\} $$

the set of **positive witnesses**<fnref n="4" /> for $x_A$, i.e. those concrete configurations of $\sigma$ for which there exists a **positive** symmetry to the chosen representative $\underline{x}_A$. The **positivity** requirement morally fixes the identity of each Opponent move, factoring out Opponent reindexing but still letting us see the Player behaviour. We now have

$$ \mathrm{wit}_{\tau}^{+} \left( \begin{pmatrix} \underline{q}^{-} & \underline{q}^{-} \\ \underline{q}^{+} & \underline{q}^{+} \end{pmatrix} \right) = \left\{ \left( \begin{pmatrix} \underline{q}_{0}^{-} & \underline{q}_{1}^{-} \\ \underline{q}_{0,f(0)}^{+} & \underline{q}_{1,f(1)}^{+} \end{pmatrix}, \begin{pmatrix} \underline{q}_{0}^{-} & \underline{q}_{1}^{-} \\ \underline{q}_{0,f(0)}^{+} & \underline{q}_{1,f(1)}^{+} \end{pmatrix}, \begin{pmatrix} \underline{q}_{0}^{-} & \underline{q}_{1}^{-} \\ \underline{q}_{0,f(0)}^{+} & \underline{q}_{1,f(1)}^{+} \end{pmatrix}, \begin{pmatrix} \underline{q}_{0}^{-} & \underline{q}_{1}^{-} \\ \underline{q}_{0,f(0)}^{+} & \underline{q}_{1,f(1)}^{+} \end{pmatrix} \right) \right\} $$

a set of concrete configurations of cardinal 4, solving the mismatch.

In [Clairambault and Paquet, 2021] we detail this, which involves delving into an intricate analysis of symmetries in concurrent games. Thanks to this we are able to correct the interpretation-preserving functor $(-) : \mathrm{ProbNTCG-Vis} \to \overline{\mathbb{R}}_{+} \cdot \mathrm{Rel}$ of [Castellan et al., 2018b]: the correct definition turns out to be given by

$$ (\boldsymbol{\sigma})_{x_A} = \sum_{x^{\sigma} \in \mathrm{wit}_{\sigma}^{+}(x_A)} v_{\sigma}(x^{\sigma}), $$

summing over *positive witnesses* rather than symmetry classes<fnref n="5" />. Beyond probabilistic weights, we prove this for games and relations weighted by arbitrary semirings of resources, modulo mild hypotheses. An interesting case is the interpretation of PCF in $\overline{\mathbb{N}}$-Rel, the relational model weighted by natural numbers. If $\vdash M : A$ is a term, to each $a \in [A]$, $[M]_a$ is a natural number, which might be arbitrarily high. So the relational model *counts* something, but what? It turns out from our study that the weighted relational model counts *positive witnesses* in the sense of concurrent game semantics.

Finally, in [Clairambault and de Visme, 2020], we also apply these ideas for the quantitative collapse of quantum strategies onto the quantum relational model.

### 13.3.2 Generalized species of structure

Interpreting programs in **TCG** allows us – for each point of the web in the sense of relational semantics – to replace a *natural number*, as given by the weighted relational model, with a *set of witnesses*. This is an example of what is increasingly being called *proof-relevant denotational semantics*; which beyond collecting behaviours, tracks, for each possible behaviour, a set of *witnesses*. The main example of such a model is the cartesian closed bicategory of *generalized species of structure* [Fiore et al., 2008].

<footnote n="4">⁴The cardinal of $\mathrm{wit}_{\sigma}^{+}(x_A)$ does not depend on the representative, provided it satisfies a condition called *canonicity*, not covered here, see [Clairambault and Paquet, 2021].</footnote>

<footnote n="5">⁵One can sum over symmetry classes, with correcting coefficients: $(\boldsymbol{\sigma})_{x_A} = \sum_{x^{\sigma} \in \mathrm{wit}_{\sigma}^{+}(x_A)} \frac{\#\delta_{-(x_A)}}{\#\delta(x^{\sigma})} \cdot v_{\sigma}(x^{\sigma})$.</footnote>
At the time (2021-2022), there was intense activity, in the quantitative semantics community, around species of structure. Roughly speaking, species of structure are a categorification of the relational model. The objects of **Rel**, i.e. sets, are replaced with categories. The morphisms of **Rel**, i.e. functions $\alpha : A \times B \to \{0, 1\}$ are replaced with

$$ \alpha : A^{\text{op}} \times B \to \text{Set}, $$

i.e. profunctors from $A$ to $B$. The bang of **Rel**, which to any set associates its set of finite multisets, is replaced with the free symmetric monoidal category. Altogether, to a program $\vdash M : A$ and some $a \in A$, the interpretation of $M$ associates a set $[[M]]_a$ – notably, Federico Olimpieri proved [Olimpieri, 2021] that this set could be presented as the set of derivations of $M : a$ in a non-idempotent intersection type system.

As two “proof-relevant” denotational models, it was appealing to try to understand the links between concurrent games and generalized species of structure. As generalized species of structure replace the coefficient computed by the weighted relational model with a set, it is tempting to conjecture that the two agree – that the coefficient given by the weighted relational model is the cardinal of the witnesses given by generalized species. But it is easy to see that this is not true: for instance, for any set $A$ we have

$$ (\mathrm{id}_A)_{a,a'} = \begin{cases} 1 & \text{if } a = a', \\ 0 & \text{otherwise} \end{cases} $$

for the identity in the weighted relational model, compared with $(\mathrm{id}_A)_{a,a'} = A[a, a']$ given by the hom-functor, the identity in the bicategory of profunctors. We can plainly see that species of structures import morphisms of $A$ as witnesses, whereas the weighted relational model does not. From the perspective of concurrent games these morphisms are nothing but the *symmetries* between configurations, so it seems that witnesses in the sense of generalized species of structure should correspond to witnesses in the sense of concurrent games *along with* explicit symmetries, i.e. for a strategy $\sigma : A \vdash B$,

$$ (\sigma)(x_A, x_B) = \{(\theta_A^-, x^\sigma, \theta_B^+) | \theta_A^- : x_A \cong_A^- x_A^\sigma, x^\sigma \in \mathcal{C}^+(\sigma), \theta_B^+ : x_B^\sigma \cong_B^+ x_B\}. $$

Though defined on configurations, this can turned be into a profunctor

$$ (\sigma) : \mathcal{S}(A)^{\text{op}} \times \mathcal{S}(B) \to \text{Set} $$

from the groupoid $\mathcal{S}(A)$ of symmetries of $A$, to that on $B$ – the functorial action is an elaboration of Lemma 7.2.7. With significant effort with Hugo Paquet and Federico Olimpieri, we proved in [Clairambault et al., 2023a] that this yields a pseudofunctor from a cartesian closed bicategory of thin concurrent games (with visible strategies, so as to cope with deadlocks) into that of generalized species of structure. It turns out that up to isomorphism, generalized species of structure can be seen as computing positive witnesses in the sense of concurrent games, along with explicit positive symmetries! This is striking, as species of structure were invented between any of those. This also shows that the cardinality mismatch between the weighted relational model and generalized species of structure exactly amounts to the number of positive symmetries.
This is a new step in the relational collapses of games model, refining earlier work
in that it is proof-relevant, and operates at the bicategorical level. It also emphasizes
that the combinatorial core of proof-relevant models is their handling of symmetries,
and there is an incredible wealth of mathematical structures to be worked out here, in
which thin concurrent games play a central role. This is also strongly connected to the
coefficients appearing in the Taylor expansion of $\lambda$-terms, see the next section.

**13.4 Game Semantics as Taylor Expansion**

This line of work is in collaboration with Lison Blondeau-Patissier, as part of her PhD
thesis (2021-2024), and with Lionel Vaux Auclair.

**13.4.1 Pointer concurrent games and positional injectivity**

As we have seen, thin concurrent games provide an expressive representation of the
interactive behaviour of programs, but at the cost of a significant technical complexity
– a lot of which comes from copy indexing and uniformity. Could we conceivably
simplify this by adopting an “Hyland-Ong” style representation, with pointers? It turns
out that we can to an extent, losing some features such as non-derministic branching, but
gaining some such as a compelling connection with the Taylor expansion of $\lambda$-terms.

The idea is the following: instead of a concurrent strategy $\sigma$, we retain only its set of symmetry classes of (+-covered) configurations, which must hence be defined directly, without appealing to all the technology of Part II. To do that we start with:

**Definition 13.4.1.** Consider A an arena in the sense of Definition 3.1.3.

An exploration<sup>6</sup> $x \in \mathscr{E}(A)$ of arena $A$ is $x = (|x|, \le_x, \partial_x)$ such that $(|x|, \le_x)$ is a finite forest, and the **display map** $\partial_x : |x| \to |A|$ is a function satisfying the conditions:

minimality-respecting: for any $a \in |x|$, $a$ is $\le_x$-minimal iff $\partial_x(a)$ is $\le_A$-minimal,

causality-preserving: for all $a_1, a_2 \in |x|$, if $a_1 \to_x a_2$ then $\partial_x(a_1) \to_A \partial_x(a_2)$.

If $A$ is a mixed board, then explorations of $\underline{A}$ are analogous to configurations of $A$: they serve as concrete representatives for symmetry classes. A **symmetry** between explorations $x, y \in \mathscr{E}(A)$ is a bijection $\phi : |x| \approx |y|$ that preserves and reflects all structure. This lets us define **positions** as symmetry classes of explorations – if $A$ is a mixed board without conflict, those are in one-to-one correspondence with $\mathscr{C}\cong(A)$.

But one should not immediately quotient explorations to positions, because doing
so blurs out the identity of individual moves, preventing us from enriching it with the
dynamic causality from the program. Instead those are added on *explorations*:

**Definition 13.4.2.** An *augmentation* on arena *A* is a tuple *q* = ⟨|q|, ≤<sub>q</sub>, ≤<sub>(|q|)</sub>, ∂<sub>q</sub>⟩, where

<footnote n="6"><sup>6</sup>In the published papers, we call those *configurations*. Here, I use *exploration* instead to avoid the collision
with the configurations of an event structure.</footnote>
<figure><img src="image_241.png" /><figcaption>Figure 13.9: A configuration</figcaption></figure>

<figure><img src="image_242.png" /><figcaption>Figure 13.10: An isogmentation</figcaption></figure>

($|q| = \langle |q|, \le_{(|q|)}, \partial_q \rangle \in \mathscr{C}(A)$, and $\langle |q|, \le_q \rangle$ is a forest$^7$ satisfying:

rule-abiding: for all $a_1, a_2 \in |q|$, if $a_1 \le_{(|q|)} a_2$, then $a_1 \le_q a_2$,

courteous: for all $a_1 \to_q a_2$, if $\mathrm{pol}(a_1) = +$ or $\mathrm{pol}(a_2) = -$, then $a_1 \to_{(|q|)} a_2$,

deterministic: for all $a^- \to_q a_1^+$ and $a^- \to_q a_2^+$, then $a_1 = a_2$,

+-covered: for all $a \in |q|$ maximal in $q$, we have $\mathrm{pol}(a) = +$,

negative: for all $a \in \min(q)$, we have $\mathrm{pol}(a) = -$,

we then write $q \in \mathcal{A}(A)$, and call $(|q|) \in \mathscr{C}(A)$ the **desequentialization** of $q$.

An augmentation equips an exploration of the game with the causal dependency due to the program. In particular, if $\boldsymbol{\sigma} : A$ is a causal strategy on a mixed board $A$, then any $x^{\boldsymbol{\sigma}} \in \mathscr{C}(\boldsymbol{\sigma})$ gives rise to an augmentation $q \in \mathcal{A}(A)$ on $\bar{A}$ by setting $|q| = x^{\boldsymbol{\sigma}}$, $s_1 \le_q s_2$ iff $s_1 \le_{\boldsymbol{\sigma}} s_2$, $s_1 \le_{(|q|)} s_2$ iff $\partial_{\boldsymbol{\sigma}} s_1 \le_A \partial_{\boldsymbol{\sigma}} s_2$, and for all $s \in |q|$, $\partial_q s = \mathrm{lbl}_A(\partial_{\boldsymbol{\sigma}} s)$.

In thin concurrent games, all events have a distinct identity and yield a distinct image in the game with distinct copy indices, as illustrated in Figure 13.9; this rigidity is then tamed by 2-cells mediating between strategies. In contrast, in pointer concurrent games, individual events have no identity; just like elements of a multiset have no individual identity. This is illustrated in Figure 13.10, but it is not properly captured yet by Definition 13.4.2 – it remains to quotient out the identity of events. For that, a **symmetry** between augmentations $q$ and $p$ is a bijection $\varphi : |q| \approx |p|$ preserving and reflecting all structure. Finally, an **isogmentation** is a symmetry class of augmentations; and then strategies should morally be certain aggregations of isoglementations.

Our original motivation in developing these definitions was not really to define a fully-fledged variant of concurrent games, but rather to obtain the tools we needed to prove an *injectivity theorem* [Blondeau-Patissier and Clairambault, 2021] along the following lines. Consider $\sigma, \tau : A$ two total finite innocent strategies in the Hyland-Ong sense. Each play $s \in \sigma$ reaches a *position* obtained by simply forgetting the chronological order; so that for each strategy we can retain its set of positions only. Now the theorem is that if $\sigma$ and $\tau$ reach the same positions, then they are equal. Now proving

<footnote n="7">⁷For now, we have only explored pointer concurrent games in a sequential innocent setting – of course, there is no reason why the methodology would not extend further.</footnote>
that involves a *pumping* technique similar to that used in traditional injectivity results in the linear logic literature [de Carvalho and de Falco, 2012], which needed understanding the effect of Opponent duplications on reached positions – and in turn, this invited a representation of plays factoring out Opponent’s scheduling, i.e. isogmentations<fnref n="8" />.

### 13.4.2 Isogmentations and the resource calculus

It is natural to see in isogmentations a variation of *resource terms*, the terms of the finitary calculus called *resource calculus* used as target for the Taylor expansion of $\lambda$-terms [Ehrhard and Regnier, 2008] – this observation was nothing new, the similarity between resource terms and plays up to Melliès’ homotopy had already been remarked before [Melliès, 2006, Tsukada and Ong, 2016]. For instance, along this similarity, the isogmentation in Figure 13.10 could be naturally be written syntactically as

$$ \lambda f^{o \to o} . f [\lambda x^o . x, \lambda x^o . x] [\lambda x^o . x]. $$

More precisely, there is a bijection between isogmentations on (the arena for) a simple type A, and $\beta$-normal resource terms in a simply-typed extensional resource calculus – moreover the correspondence is straightforward, closely following the standard finite definability argument for innocent strategies (see Theorem 3.2.14) – but this correspondence does not account for non-normal terms and for the dynamics of resource terms.

To account for these dynamics, one difficulty is that isogmentations do not easily compose. Indeed, we expect isogmentations $q \in \mathcal{A}(A \vdash B)$ and $p \in \mathcal{A}(B \vdash C)$ to be *composable* if, writing $\langle q \rangle = x_A \vdash x_B$ and $\langle p \rangle = y_B \vdash y_C$ for the corresponding positions, we have $x_B = y_B$ – so that we may write $\langle q \rangle = x_A \vdash x_B$ and $\langle p \rangle = x_B \vdash x_C$. In that case, up to symmetry we can pick concrete representatives for $q$ and $p$ which share the same events on $B$, letting us synchronize them. However, this idea bumps against an issue similar to that exposed in Example 13.3.1: the resulting composition depends on the representative chosen... To eliminate this dependency on the representative, we first define a composition $p \odot q$ through a symmetry $\theta : x_B \cong_B y_B$, and then set

$$ p \odot q = \sum_{\theta : x_B \cong_B y_B} p \odot \theta q $$

a *formal sum* of isogmentations. This observation – that the composition of isogmentations yields a formal sum of isogmentations, rather than a single isogmentation – is reminiscent of the fact that substitution is the resource calculus also yields a sum

$$ s\langle [u_1, \dots, u_n]/x \rangle = \sum_{\pi \in S(n)} s\langle u_{\pi(1)}/x_1 \rangle \dots \langle u_{\pi(n)}/x_n \rangle $$

if $x$ has $n$ occurrences in $s$ (the result is 0 otherwise) – where $x_1, \dots, x_n$ is an enumeration of all occurrences of $x$ in $t$. This prompted us to extend the correspondence between isogmentations and normal resource terms to the *dynamics* of the resource calculus.

<footnote n="8">⁸In other terms, isogmentations are plays up to Melliès’ homotopy equivalence on plays [Melliès, 2006].</footnote>
This is what we achieve in [Blondeau-Patissier et al., 2023b]: we construct an interpretation of (simply-typed, extensional) resource terms as **strategies**, i.e. formal sums of isoglementations weighted by non-negative rational coefficients. For normal forms, this coincides with the bijection between normal resource terms and isoglementations mentioned above. But for non-normal terms, we show that the interpretation is invariant under reduction – also accounting for the coefficients arising throughout reduction. The proof of this result is structured by a new categorical model we call a **resource category**. Resource categories axiomatize the structure available in our category of pointer concurrent games. Much of their structure resembles notions of differential categories [Blute et al., 2020], but without an exponential modality.

### 13.4.3 Taylor expansion, extensional resource terms

The correspondence between normal resource terms and isoglementations invites the conjecture that the game semantics of a $\lambda$-term *is* the normal form of its Taylor expansion.

But the Taylor expansion typically targets the *pure* $\lambda$-calculus, for which this is not quite true: game semantics is an extensional model, while the Taylor expansion of a $\lambda$-term follows its *Böhm tree* (i.e., the normal form of the Taylor expansion of a $\lambda$-term *M* is the Taylor expansion of its Böhm tree, as proved in [Ehrhard and Regnier, 2003]. So what we did instead is to devise a variant of the untyped resource calculus, the *extensional resource calculus*, obtained by seeking a syntax for the isoglementations on the universal arena of [Ker et al., 2002]. The extensional resource calculus has a nice syntactic theory, and is the target of an *extensional Taylor expansion* that captures $H^*$ [Blondeau-Patissier et al., 2023a]. At the date of writing, the correspondence of this extensional Taylor expansion with pointer concurrent games is still work in progress.

## 13.5 Operational Concurrent Games

This line of work is in collaboration with Simon Castellan.

**Operationalizing a denotational model.** As hopefully demonstrated in this monograph, thin concurrent games offer a very expressive intensional presentation of the interactive behaviours of programs. The work presented here already accounts for complex programming features, and there is no obstacle in principle to extend it further.

Yet, something is puzzling. More than any other denotational semantics, game semantics has a strong operational flavour. To the trained game semanticist, each play or configuration of the interpretation of a program matches an operational execution trace: it is this informal connection that guided our introduction to game semantics in Chapter 3. Yet, actually *proving* that a concrete play or configuration is in the interpretation is discouragingly – and embarrassingly – tricky: one must unfold the definition of the interpretation of a $\lambda$-term in a cartesian closed category, which is itself obtained as the Kleisli category of a model of intuitionistic linear logic. Overall, the interpretation of a program unfolds to a large algebraic expression in the language of the categorical model
<figure><img src="image_243.png" /><figcaption>Figure 13.11: Is this a valid configuration for this program?</figcaption></figure>

– for instance, the program of Figure 13.11 (partially) unfolds to an expression like

$$ \mathrm{seqo}((\mathrm{ev} \circ ((\llbracket F \rrbracket \otimes \llbracket x :=!y; F (y := 1) \rrbracket^1) \circ (\delta \otimes \mathrm{id} \otimes \mathrm{id}))) \otimes \llbracket !x \rrbracket) \circ (\mathrm{id} \otimes \delta \otimes \mathrm{id}) \circ (\mathrm{id} \otimes \mathrm{cell} \otimes \mathrm{cell}), $$

and answering the question in Figure 13.11 means putting forward an analogous configuration for each of the components of this expression, and proving they globally aggregate to the configuration claimed: this is not problematic in principle, but not efficient or even tractable in practice, so it is an obstacle to using game semantics to reason on concrete programs. Game semantics papers are full of examples, yet I feel confident in claiming that none but a few trivial ones have ever been proved formally<fnref n="9" />.

It seems we must choose between an interpretation that is compositional and one that it obtained directly operationally from the program. Or; we could try to devise an alternative – operational – method to generate the denotational object. Connecting operational and game semantics in that way is far from a new idea. Though it was clear from early work on game semantics [Danos et al., 1996] that interaction between strategies was related to execution by abstract machines, the idea to generate strategies by operational means was – to our knowledge – first suggested by Laird in his trace semantics for higher-order references [Laird, 2007] (with the explicit connection with game semantics later worked out by Jaber [Jaber, 2015]). In the 2010s, several works were proposed blurring the lines between operational and game semantics [Ghica and Tzevelekos, 2012, Levy and Staton, 2014], typically via LTSs dealing with open programs by sending and receiving messages from the environment; for these systems, compositionality is a theorem rather than a definition. But these developments do not yield strategies in the sense of previously established models. They also only deal with sequential deterministic programs, and it seems hard to extend LTS-based techniques to give a causal account of the execution of higher-order concurrent programs.

<footnote n="9">⁹This observation is meant to apply to all the game semantics literature, not just concurrent games.</footnote>
But in fact, a powerful connection between operational and denotational semantics was already established significantly before the above, although not then presented as such: it is Baillot’s result [Baillot, 1999] that Girard’s *Geometry of Interaction* for IMELL generates the strategy obtained as its interpretation in so-called Abramsky-Jagadeesan-Malacaria (AJM) games [Abramsky et al., 2000]. We would like a similar correspondence for concurrent games as presented in this monograph. But how so? Geometry of Interaction is based on linear logic proof nets and Baillot’s theorem relies on the rewriting theory of proof nets, but there are no such tools for $IA_\parallel$.

**Geometry of Interaction via Petri nets.** In [Castellan and Clairambault, 2023] we ask the question: can we provide an analogue of Baillot’s theorem for $IA_\parallel$, i.e. a notion of execution for $IA_\parallel$ programs that generates, just as a side effect of execution, the *same* concurrent strategy than that computed denotationally?

Our idea is the following: while there are no proof nets for $IA_\parallel$, a proof net *equipped with the GoI token game* is an instance of an object that is very well-known in the verification and concurrency communities: a *coloured Petri net*. So we sidestep proof nets and aim to translate $IA_\parallel$ programs directly into Petri nets. More precisely, we devise a notion we call a *Petri strategy*: a Petri strategy on game *A* is a (finite) coloured Petri net equipped with special transitions called *negative* and *positive* (on top of the old transitions now dubbed *neutral*). While neutral transitions have the same familiar mechanics as usual, negative and positive transitions are different: negative transitions have no precondition, instead triggered by an Opponent move in *A* and introducing a new token into the net. Dually, positive transitions have no postcondition, instead playing a positive move in *A*. Now, Petri nets satisfying adequate conditions support a notion of *unfolding* into event structures: each run has an implicit causal structure and those can be aggregated into an event structure. Accordingly, a *Petri strategy* is additionally required to unfold to a valid concurrent strategy. Finally, Petri strategies $\sigma$ and $\tau$ can be easily composed, by putting them side by side and merging adequately matching negative and positive transitions. Altogether, we obtain a compositional interpretation of $IA_\parallel$ into Petri strategies and an unfolding to concurrent strategies, such that

<figure><img src="image_244.png" /></figure>

commutes. The interpretation of $IA_\parallel$ into Petri nets is linear time, and can be regarded as a syntactic translation – a compilation – to an intermediate representation.

This is implemented and available at https://ipatopetrinets.github.io/. A screenshot of the application appears in Figure 13.12: on the right hand side we have the Petri strategy, with which the user can interact by clicking on available transitions. On the upper left corner is the program, and below is the configuration of the corresponding concurrent strategy reconstructed by the unfolding. The configuration is that of Figure 13.11 which, by our main result, proves that this is indeed a configuration of
<figure><img src="image_245.png" /><figcaption>Figure 13.12: IA<sub>∥</sub> to Petri nets</figcaption></figure>

the concurrent strategy interpreting this program. Thanks to the causal nature of our interpretation, there is also a *reverse mode* that let us *undo* events, not necessarily in the opposite order in which they were played.

## 13.6 Miscellaneous

Finally, in this section, I give an account of other works that stand a bit on the side: though interesting, they are not part of the main thrust of our work on concurrent games.

### 13.6.1 Full Abstraction for Parallel-Or

This is joint work with Simon Castellan and Glynn Winskel.

In Chapter 10, I have presented our notion of parallel innocence, culminating in Chapter 12 to finite definability and intensional full abstraction for PCF<sub>∥</sub>. But in fact, our original objective was *not* PCF<sub>∥</sub>, but PCF plus *parallel-or*, the famous parallel primitive

$$ \mathbf{por} \ ff \ ff = \ ff $$

$$ \mathbf{por} \ tt \perp = \ tt $$

$$ \mathbf{por} \perp tt = \ tt $$

introduced by Plotkin in order to obtain a finite definability result with respect to Scott domains and continuous functions [Plotkin, 1977]. A central motivation in the original development of game semantics was precisely to ban **por** and obtain a cartesian closed category of sequential functions, and thus it felt deliciously ironic to attempt to close the
<figure><img src="image_246.png" /><figcaption>Figure 13.13: The concurrent strategy *por*: $B_1 \dashv B_2 \dashv B_3$</figcaption></figure>

loop and capture the intensional behaviour of programs from PCF+por. Unfortunately, back in 2014, we bumped against a tricky problem and could not quite make this work.

Let us describe the problem. There is a natural concurrent strategy for **por**, described in Figure 13.13. When prompted by Opponent, the strategy plays two causally independent moves, prompting the evaluation of its two arguments in parallel. If both arguments return **ff**, then the strategy merges those two threads and returns **ff**. However, it suffices that *one* argument returns **tt** for the overall computation to return **tt**. What may come as a surprise is that although the extensional behaviour of **por** is functional (and thus deterministic), its intensional behaviour as given by this strategy is not. Indeed, each argument returning **tt** must cause an independent instance of the answer **tt** at toplevel. But those must conflict, since they match the same move in the game! In other words,

**por tt tt**

triggers an (invisible) race as the two threads compete to provide the same answer – operationally, **por tt tt** can be proved via two distinct rules, also witnessing this race.

How to formulate a notion of determinism accepting **por**, but refusing an actual non-deterministic choice? We could not figure out how to solve this back in 2014, hence reverted in [Castellan et al., 2015] to giving a model giving account of (causally deterministic) parallel evaluation in plain PCF.

**Disjunctive causality.** In [Castellan et al., 2017b] we solved that, constructing an intensionally fully abstract model for (an affine version of) PCF with **por**. The core of our solution is a variant of **CG** in which the semantics of **por** is *deterministic*.

The reasons why **por** is deterministic run quite deep: it boils down to the inability of event structures to express *disjunctive causality*, i.e. causal patterns such as

<figure><img src="image_247.png" /></figure>
where the *same* event 3 may be caused *either* by 1 or by 2. But in fact, this is not a limitation of event structures in general, only of event structures of the kind we consider in this monograph, which are known as *prime event structures* in the literature. There are alternatives: for instance, *general event structures* [Winskel, 1980] allow events to be enabled in several distinct ways. We give an equivalent notion [Winskel, 1986]:

**Definition 13.6.1.** A configuration family is a pair ($|A|$, $A$) (often just written $A$) where $|A|$ is a set of events, and $A$ is a set of configurations, finite subsets of $|A|$ satisfying:

rooted: $\emptyset \in A$

complete: for $x, y \in A$, if $x \uparrow y$ (*they are compatible*, i.e. there exists $z \in A$ such that $x \subseteq z$ and $y \subseteq z$), then $x \cup y \in A$.

coincidence-free: if $x \in A$, for all distinct $e_1, e_2 \in x$ there exists $y \subseteq x$ such that $y \in A$ and $e_1 \in y \Leftrightarrow e_2 \notin y$.

Configuration families do support disjunctive causality: the causal pattern of (13.3) is expressible with the configuration family with events {1, 2, 3} and the configurations

$$ \{\emptyset, \{1\}, \{2\}, \{1, 3\}, \{2, 3\}, \{1, 2, 3\}\}, $$

and accordingly, *parallel-or* can be formalized as a configuration family that is *deter- ministic* in a suitable sense. So – why is this monograph entirely phrased in terms of configuration families, rather than prime event structures? The issue with configuration families is that they do not support *hiding* as is required in the composition of strategies:

**Proposition 13.6.2.** *Configuration families do not support hiding. There is a configuration family A and $V \subseteq |A|$ s.t. $\{x \cap V \mid x \in A\}$ is not a configuration family.*

*Proof.* Set $|A| = \{a, b, c, d\}$, and configurations those specified by the diagram

<figure><img src="image_248.png" /></figure>

with $V = \{b, c, d\}$, i.e. we hide the event $a$. Then, the set of configurations obtained by hiding fails completeness: it contains $\{b\}$, $\{d\}$, $\{b, c, d\}$ but not $\{b, d\}$. $\square$

Prime event structures support hiding because each event in the event structure post-hiding comes with a *unique, minimal* causal history in the event structure pre-hiding, a property that is lost here<fnref n="10" />. The failure of hiding comes from our inability to assign canonically, to any configuration of the hidden structure, a *witness* pre-hiding.

<footnote n="10">¹⁰One could object here that perhaps we could build concurrent games on something even more permis- sive than configuration families. But we must retain *coincidence-freeness*, because they are how we express the absence of causal loops (which distinguish concurrent games from relational semantics as illustrated in Section 10.4): any configuration should be reachable adding events one by one. Rooted coincidence-free families do support hiding, but they yield a non-associative composition of strategies.</footnote>
**Observational determinism.** The key idea of our contribution is that we can recover hiding on configuration families, by requiring an additional *determinism* hypothesis:

**Definition 13.6.3.** A deterministic configuration family with polarities (dcfp) is a configuration family A with $\text{pol}_A : |A| \to \{-, 0, +\}$, satisfying the additional condition:

disjunctive deterministic: for all $x \subseteq_A^{\ge 0} y$ and $x \subseteq z$, we have $y \cup z \in A$.

where $x \subseteq_A^{\ge 0} y$ means that $x \subseteq y$ and $\text{pol}_A(y \setminus x) \subseteq \{0, +\}$.

Here, the events with null polarities are those that we wish to hide, and indeed:

**Proposition 13.6.4.** If A is a dcfp, then its **hiding** $A_\downarrow$, with events the set $V = \{a \in A | \text{pol}(a) \neq 0\}$ and configurations those $x \cap V$ for $x \in A$, is still a dcfp.

The key idea is as follows: a configuration $x \in A_\downarrow$ may have many different witnesses, i.e. configurations $y \in A$ such that $y \cap V = x$ – in general forming a family $(y_i)_{i \in I}$. But thanks to disjunctive determinism, all these witnesses are *compatible*, and

$$y = \bigcup_{i \in I} y_i \in A$$

is then a *canonical witness* for $x$. As in prime event structures, it is this ability to assign canonically to each $x \in A_\downarrow$ a witness in $A$ that makes hiding go through. The situation here is somewhat dual to that for prime event structures: the canonical witness is the union of all witnesses, instead of the intersection as in the construction of **CG**.

Replaying the construction of **CG** based on the ideas above yields a compact closed category **Disj** of **disjunctive deterministic strategies**, where **por** admits a deterministic interpretation. In [Castellan et al., 2017b] we then proceed to build a hybrid model pairing **Disj** and **CG**, so that we have access to both disjunctive determinism and parallel innocence, letting us prove a finite definability result and intensional full abstraction.

## 13.6.2 A Semantic Proof of Herbrand's Theorem

This is joint work with Aurore Alcolei, Martin Hyland and Glynn Winskel.

In a formula of (first-order) predicate logic, there is a clear causal dependency between instance of quantifiers that may be represented as a concurrent game, e.g.

$$[\forall x (\exists y P(x, y) \lor \forall z \neg P(x, z))] = \begin{array}{c} \forall x \\ \exists y \\ \phantom{\exists} \forall z \end{array}$$

though this representation ignores for now all propositional connectives and atomic predicates. Then, a proof intuitively induces a further dependency between instances
of quantifiers that may be represented with a concurrent strategy; for instance we have

$$ \left[ \frac{\frac{\frac{\vdash P(x, z) \lor \neg P(x, z)}{\vdash \exists y P(x, y), \neg P(x, z)}}}{\frac{\frac{\vdash \exists y P(x, y), \forall z \neg P(x, z)}{\vdash \exists y P(x, y) \lor \forall z \neg P(x, z)}}}{\vdash \forall x (\exists y P(x, y) \lor \forall z \neg P(x, z))} \right] = \vcenter{\ Diagram(0,0)(100,100)% \node at (0,0) {\begin{tabular}{c} $\forall x$ \\ $\exists y \llcorner$ \\ $\neg z$ \end{tabular}}(100,0)% \node at (100,0) {\begin{tabular}{c} $\forall y \llcorner$ \\ $\neg z$ \end{tabular}}(100,100)% \node at (100,100) {\begin{tabular}{c} $\forall x$ \\ $\neg y$ \\ $\lor z$ \end{tabular}}(0,100)% \node at (0,100) {\begin{tabular}{c} $\forall y$ \\ $\neg z$ \\ $\land x$ \end{tabular}}(0,0)% \node at (0,0) {\begin{tabular}{c} $\forall x$ \\ $\neg y$ \\ $\lor z$ \end{tabular}} \right] $$

witnessing the fact that the proof instantiates $y$ with the eigenvariable $z$. The strategy only carries this causal dependency between quantifiers; the two players do not, for instance, play elements of a given structure in which the formula is evaluated, as would be the case in usual notions of games in the context of model theory.

We must still account for predicates and propositional connectives. To figure out whether such a strategy is correct, or *winning* in our terminology, we instantiate quantifiers following the dependency specified in the strategy, yielding a quantifier-free formula for which we assess whether it is a propositional tautology. In the example above, the causal dependency $\forall z \rightarrow \exists y$ in the strategy expresses that $y$ should be replaced with $z$. Performing this substitution (and removing quantifiers), we obtain the formula

$$ P(x, z) \lor \neg P(x, z) $$

which is a propositional tautology indeed, so the strategy is winning.

**Strategies with witnesses.** Beyond simply substituting one variable for another, a proof can instantiate an existential quantifier with a *first-order term*. Accordingly a strategy provides, for each positive move (existential quantifier), a first-order term whose free variables are the eigenvariables introduced by the universal quantifiers.

For instance, a variation of the example above could be

$$ \left[ \frac{\frac{\frac{\vdash P(x, f(z)) \lor \neg P(x, f(z))}{\vdash \exists y P(x, y), \neg P(x, f(z))}}}{\frac{\frac{\vdash \exists y P(x, y), \forall z \neg P(x, f(z))}{\vdash \exists y P(x, y) \lor \forall z \neg P(x, f(z))}}}{\vdash \forall x (\exists y P(x, y) \lor \forall z \neg P(x, f(z))))} \right] = \vcenter{\ Diagram(0,0)(100,100)% \node at (0,0) {\begin{tabular}{c} $\forall x$ \\ $\exists y \llcorner$ \\ $\neg z$ \end{tabular}}(100,0)% \node at (100,0) {\begin{tabular}{c} $\forall y \llcorner$ \\ $\neg z$ \end{tabular}}(100,100)% \node at (100,100) {\begin{tabular}{c} $\forall x$ \\ $\neg y$ \\ $\lor z$ \end{tabular}}(0,100)% \node at (0,100) {\begin{tabular}{c} $\forall y$ \\ $\neg z$ \\ $\land x$ \end{tabular}}(0,0)% \node at (0,0) {\begin{tabular}{c} $\forall x$ \\ $\neg y$ \\ $\lor z$ \end{tabular}} \right] $$

decorating the quantifier $\exists y$ with the witness provided for $y$, here $f(z)$. The resulting instantiation of quantifiers yields a propositional tautology $P(x, f(z)) \lor \neg P(x, f(z))$.

**Contraction.** But classical proofs have access to the contraction rule, and as such may provide several witnesses for the same existential quantifier. So the interpretation of formulas is modified accordingly: instead of simply following the nesting of quantifiers,
it has countably many copies of each quantifier – though it is often more convenient to
only draw the part of the game where only existential quantifiers are replicated.

For instance, the strategy for the usual proof of the Drinker's formula is:

$$
\left[
  \left[
    \frac{
      \vdash \neg P(c), P(y), \neg P(y) \lor \forall y P(y)
    }
    {\vdash \neg P(c), P(y), \exists x (\neg P(x) \lor \forall y P(y))}
  \right]
  \right.
  \left[
    \frac{
      \vdash \neg P(c), \forall y P(y), \exists x (\neg P(x) \lor \forall y P(y))
    }
    {\vdash \neg P(c) \lor \forall y P(y), \exists x (\neg P(x) \lor \forall y P(y))}
  \right]
  \left.
    \frac{
      \vdash \exists x (\neg P(x) \lor \forall y P(y)), \exists x (\neg P(x) \lor \forall y P(y))
    }
    {\vdash \exists x (\neg P(x) \lor \forall y P(y))}
  \right]
  =
  \vcenter{
    \hbox{
      \begin{tabular}{@{}c@{}}
        \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
          \node (y1) at (0,0) {$\vdash$};
          \node (y2) at (0,1) {$\vdash$};
          \node (x1) at (1,0) {$\vdash$};
          \node (x2) at (1,1) {$\vdash$};
          \draw (y1) -- (y2);
          \draw (x1) -- (x2);
          \node at (0.5,0.5) {$\neg$};
          \node at (0.5,1) {$\neg$};
          \node at (0.5,-0.5) {$\forall$};
          \node at (0.5,1.5) {$\forall$};
        \end{tikzpicture}
      }
      \quad
      \begin{tabular}{@{}c@{}}
        \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}]
          \node (y1) at (0,0) {$\vdash$};
          \node (y2) at (0,1) {$\vdash$};
          \node (x1) at (1,0) {$\vdash$};
          \node (x2) at (1,1) {$\vdash$};
          \draw (y1) -- (y2);
          \draw (x1) -- (x2);
          \node at (0.5,0.5) {$\neg$};
          \node at (0.5,1) {$\neg$};
          \node at (0.5,-0.5) {$\forall$};
          \node at (0.5,1.5) {$\forall$};
        \end{tikzpicture}
      \end{tabular}
    }
  \right]
$$

assuming we have at least one constant symbol $c$ – here the existential quantifier has
two copies, witnessing the fact that the proof has a contraction. Instantiating quantifiers
following this strategy, we obtain the quantifier-free formula

$$
(\neg P(c) \lor P(y)) \lor (\neg P(y) \lor P(z))
$$

which is a tautology – here as there are two instantiations for the existential quantifier,
there are two copies of the subsequent sub-formula, linked with a disjunction.

In [Alcolei et al., 2018] we provide a denotational semantics for first-order classical
proofs following this idea. For an existential formula $\exists x P(x)$, the interpretation of a
proof corresponds exactly to a set of closed first-order terms $t_1, \dots, t_n$ such that $P(t_1) \lor
\dots \lor P(t_n)$ is a propositional tautology, recovering Herbrand's theorem. For more general
formulas, we essentially recover Miller's expansion trees [Miller, 1987].

This work is original in that of all the developments considered in this monograph,
this is the only one for which the games considered are not polarized (all minimal moves
may not have the same polarity) and where causality is not alternating.

**13.6.3 Revisiting Games Models of MALL**

As mentioned in Section 6.5, (thin) concurrent games belong to a family of games model
rejecting the hypothesis that plays should be totally chronologically ordered, initiated
in the seminal paper [Abramsky and Melliès, 1999] and used in particular to construct
a fully complete model for multiplicative additive linear logic.

Abramsky and Melliès' take on games is rather radical: their games have neither
*moves* nor *plays*, but only a partial order of *positions*. More precisely, they are *dI-domains*, i.e. directed-complete, bounded-complete partial order satisfying two further
axioms. If *D* is a *dI-domain*, we write *D*<sup>*T*</sup> its extension with a top element *T* – it fol-
loows that *D*<sup>*T*</sup> is a complete lattice. If *E* is an event structure (so that this automatically
applies to a game *A* in the sense of Definition 6.1.3), then the domain *C*<sup>*∞*</sup>(*E*) of poten-
tially infinite configurations is such a *dI-domain*. If *A* is a game, then *C*<sup>*∞*</sup>(*A*) is a new
presentation of that game retaining only positions, forgetting individual moves.
Accordingly, a strategy in the sense of Abramsky and Melliès cannot play individual moves and acts on positions instead. Applied to a position x, a strategy $\sigma$ saturates it, returning a new position that intuitively incorporates all moves that $\sigma$ is prepared to play in x (or $\top$ if the strategy is undefined on the current position). More precisely, strategies are continuous, stable closure operators<fnref n="11" /> – recall $f : D \to D'$ between di-domains is stable iff for $x, y \in D$, if $x, y$ are bounded then $f(x \land y) = f(x) \land f(y)$.

**Definition 13.6.5.** A closure-strategy on di-domain $D$, written $\sigma : D$, is a continuous stable closure operator on $D^\top$, i.e. a continuous function $\sigma : D^\top \to D^\top$ which is:

extensive: for all $x \in D^\top$, $x \le \sigma(x)$,

idempotent: for all $x \in D^\top$, $\sigma(\sigma(x)) = \sigma(x)$),

stable: there is a stable function $f : D \to D$ satisfying that for all $x \in D$ such that $\sigma(x) \neq \top$, $\sigma(x) = x \lor f(x)$.

Stable implies extensive, however we state it separately as extensive and idempotent together they define a closure operator, a standard notion independently of stability.

The strategies may be composed; and Abramsky and Melliès construct a category **ClosOp** of di-domains and closure-strategies, using which they build a fully complete model of linear logic. Naively, it might seem full completeness follows by “fixing” the non-associativity of composition in Blass games [Blass, 1992], and thus reinstating the equational laws expected of a model of MALL. In truth, the situation is more subtle: Abramsky and Melliès (implicitly) construct a model of a *polarized* version of MALL. It is then the *positionality* of strategies in **ClosOp** that allows the depolarization to MALL to induce a congruence, reinstating the desired equational laws and obtaining full completeness, as made more explicit in later work by Melliès [Melliès, 2005].

In [Clairambault, 2023], I revisit this story in the context of concurrent games on event structures. A lot of that paper consists in a synthesis of old ideas, already existing in the literature (though with a different technical underpinning).

**From event structures to closure operators.** But this article also has original contributions, with in particular the first proper treatment of the relationship between move-based game semantics and Abramsky and Melliès' model. Though the intuition seems clear, the definition is not so obvious (several incorrect attempts appear in the literature).

Given a (causally deterministic) concurrent strategy $\sigma : A$, we must define

$$ \mathrm{Clos}(\sigma) : \mathcal{C}^{\infty}(A) \to \mathcal{C}^{\infty}(A) $$

a closure-strategy. Given $x_A \in \mathcal{C}^{\infty}(A)$, by causal determinism, there is at most one $x^\sigma \in \mathcal{C}^{\infty}(\sigma)$ such that $\partial_\sigma x^\sigma = x_A$. If we can find such $x^\sigma$, then we may saturate it by taking a maximal $x^\sigma \subseteq^+ y^\sigma$, and set $\mathrm{Clos}(\sigma)(x_A) = y_A^\sigma$. But what should we do if there is no $x^\sigma \in \mathcal{C}^{\infty}(\sigma)$ such that $\partial_\sigma x^\sigma = x_A$? As it turns out, the correct answer is to play all positive moves of $\sigma$ enabled in $x_A$, even though $x_A$ might have positive moves that $\sigma$ will never play. If doing so yields a conflict, then we return $\top$.

<footnote n="11">¹¹Some additional conditions appear in the course of [Abramsky and Melliès, 1999], omitted here.</footnote>
# Chapter 14

# Conclusions

## 14.1 The Work Done so Far

What do the following works have in common?

* Hyland and Ong's fully abstract games model for PCF [Hyland and Ong, 2000],

* Abramsky and McCusker's fully abstract games model for IA based on alternating non-innocent strategies [Abramsky and McCusker, 1996],

* Abramsky and Melliès' fully complete model for MALL based on closure operators [Abramsky and Melliès, 1999],

* The relational model and its syntactic presentation, non-idempotent intersection types [Girard, 1988],

* Ghica and Murawski's fully abstract model for IA$_{\parallel}$ [Ghica et al., 2006],

* The weighted relational model [Laird et al., 2013],

* Alternating probabilistic game semantics [Danos and Harmer, 2000],

* Generalized species of structure [Fiore et al., 2008],

* The Taylor expansion of $\lambda$-terms [Ehrhard and Regnier, 2008],

* The GoI token machines [Danos and Regnier, 1996, Mackie, 1995].

The results presented in this monograph, accounting both for the work presented in details in Parts II and III and that presented more synthetically in Chapter 13, show that all these models are essentially obtained from concurrent games via forgetful operations: they are presentations of certain aspects of concurrent strategies. This list is of course a tiny fragment of denotational semantics, but this already gives a sign that we are getting closer to the *full interactive behaviour* mentioned in the introduction.
Our point is certainly not that this makes all these models obsolete. Concurrent games are too intensional for many purposes, and syntactic methods such as non-idempotent intersection types or Taylor expansion, by working directly on syntax, avoid the overhead brought by the categorical machinery of denotational semantics. More generally, different purposes call for different tools; concurrent games unifies these models but with the price of a high technical complexity which is not always desirable.

In contrast, we argue that this work strengthens all these models by inscribing them within a common semantic landscape and making them part of a joint mathematical theory. Many questions on their strengths, limitations and potential extensions can be attacked under the lens of concurrent games: for one example, how should non-idempotent intersection types and Taylor expansion of programs best deal with branching effects (such as non-determinism and parallelism) or quantitative effects (such as probabilities)? Concurrent strategies support all this and extend Taylor expansion conservatively, so the question above is reduced to the following: can concurrent games be described more syntactically, in the style of intersection types or Taylor expansion?

## 14.2 Open Problems

Next, here are some open problems around the theory presented in this monograph. Those are not necessarily long-term research objectives or directions (though some could be), but rather technical difficulties encountered during the technical developments, that we have not been able to solve and have had to avoid or work around.

### 14.2.1 Non-deterministic parallel innocence

In Chapter 10 we have developed the theory of *parallel innocent* causal strategies; but our notion of innocence (Definitions 10.1.8 and 10.1.11) smuggles in *causal determinism*, i.e. the absence of minimal conflicts between Player moves. But parallel innocence is intended to ban state and more generally side-channel interference between threads, there is no reason why it would necessarily enforce determinism. For instance, what are the strategies generated by $\mathbf{PCF}_\parallel$ plus a non-deterministic choice operator $\ominus$?

First of all, in the case of *sequential innocence* there is no problem, as spelled out in Definition 13.2.1: the problem appears only for non-deterministic *parallel* innocence. First, the conditions of Definition 13.2.1 do not work as-is: *locally sequential* is wrong for obvious reasons (as it forbids parallel branching); *locally conflicting* forbids parallelism (see Figure 13.13) which should certainly be parallel innocent.

Recall that parallel innocence started with *pre-innocence* (Definition 10.1.8), which follows the idea that Player cannot causally merge threads forked by Opponent. It is natural to attempt to follow the same idea for conflict, and define:

**Definition 14.2.1.** For A a board, a visible $\sigma$: A is \#-pre-innocent iff

\#-pre-innocence: If $m_1^+ \sim_{\sigma} m_2^+ \in \sigma$ and $\rho_1 \to m_1^+, \rho_2 \to m_2^+ \in \text{gcc}(\sigma)$, then $\min(\rho_1) = \min(\rho_2)$ and their least distinct moves are positive.
<figure><img src="image_249.png" /><figcaption>Figure 14.1: The subtlety of non-deterministic parallel innocence</figcaption></figure>

In other words, Player cannot impose conflict between threads forked by Opponent.

It is quite intuitive that strategies obtained from PCF<sub>||</sub> plus ⊢ must satisfy this, as ⊢ can only be used to generate conflict between moves that share the same causal predecessors. And for quite some time, we were convinced we had a proof that this (in the presence of visibility) was stable under composition. With that condition, it is then tempting to define parallel innocence without causal determinism but with #-pre-innocence, so that it also covers non-deterministic parallel innocence.

However, #-pre-innocence is not stable under composition. The strategy

$(o \to o) \vdash o \to o \to (o \to o \to o) \to o$

<figure><img src="image_250.png" /></figure>

is visible, pre-innocent and #-pre-innocent, but its composition with the identity on o is not, as the minimal conflict is transported to the two final positive moves, though the gccs leading to them are forked by Opponent. Therefore the open question is:

**Open question 14.2.2.** *Define a condition of non-deterministic parallel innocence.*

Non-deterministic parallel innocence should compose, and support the interpretation of PCF<sub>||</sub> with ⊢, and of parallel-or. Additionally, non-deterministic parallel innocent strategies which are causally deterministic should be parallel innocent in the sense of this monograph. Non-deterministic parallel innocent strategies which are sequential should be non-deterministic sequential innocent as in Definition 13.2.1.

In other words, the problem is to disentangle non-determinism and parallelism.

Note that non-deterministic parallel innocence is not going to be conservative with respect to deterministic parallel innocence (which probably means that we do not have
deterministic parallel innocence quite right either) as illustrated in Figure 14.1. By composing a deterministic parallel innocent strategy with a sequential non-deterministic innocent strategy (that is obviously definable in a non-deterministic linear $\lambda$-calculus with non-deterministic choice), we break #-pre-innocence. Something is wrong with the deterministic parallel innocent strategy of Figure 14.1, but it seems that it cannot be banned with simple, local forbidden patterns as in pre-innocence and #-pre-innocence; our best guess is a global correctness criterion in the style of linear logic proof nets.

Once equipped with a satisfactory notion of non-deterministic innocence, it would be natural to further seek a corresponding extension of the sequential probabilistic innocence of Definition 13.2.2 to a full parallel probabilistic innocence.

## 14.2.2 Proper determinism

An issue strongly related to proper non-deterministic parallel innocence, is that of determinism. As we have seen, IA<sub>‖</sub> is a genuinely non-deterministic language, due to the combination of parallelism and state causing races in the memory. Accordingly, in Part III, our conditions of *parallel innocence* and *sequentiality* each had to reimpose determinism; but this was done is radically different ways.

Recall indeed *causal determinism*, a part of parallel innocence:

**Definition 10.1.1.** Consider $\sigma : A \vdash B$ a causal strategy.

We say $\sigma$ is **causally deterministic** if for all $s \sim_{\sigma} s'$ in $\sigma$, $\text{pol}(s) = \text{pol}(s') = -$.

And recall also *sequential determinism*, a part of sequentiality:

**Definition 11.1.4.** A strategy $\sigma \in \text{NTCG}(A, B)$ is sequential if:

pointed: if $s \in \sigma$, there is a unique $\text{init}(s) \le_{\sigma} s$ minimal in $\sigma$,

sequential determinism: if $tn_1^+, tn_2^+ \in \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$, then $n_1 = n_2$,

sequential visibility: if $s \in \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$, writing $\lceil s \rceil = s_1 \dots s_n$ and $1 \le j \le n$, if $s_j$ is non-minimal then there is $1 \le i < j$ s.t. $j(s_j) = s_i$,

where the justifier $j(m)$ of $m \in \sigma$ refers to Definition 10.2.1.

**Open question 14.2.3.** Define a proper notion of determinism, unifying these two.

Note that such a proper determinism *should not be compositional* – indeed both IA and PCF<sub>‖</sub> are deterministic languages, but their union is not. However, proper determinism should become compositional in conjunction with either non-deterministic parallel innocence and non-deterministic sequentiality.

As a reasonable starting point, it might be that in the presence of (an appropriate notion of) non-deterministic parallel innocence, *sequential determinism* implies causal determinism. Indeed, proving that amounts to showing that all Player immediate conflicts are reachable in an alternating linearization, which seems plausible, if conflicting patterns are anything like the *globules* of Definition 10.5.1.
### 14.2.3 All well-bracketings

Rather than the clear statement of an open problem, this is a description of an unfortunate state of affairs in this monograph: namely, the status of well-bracketing – understood broadly as a constraint on the function call/return discipline. In this monograph, we have seen four different mechanisms akin to well-bracketing.

Firstly, of course, we have seen the traditional **chronological well-bracketing** of Section 3.2.2, explicitly requiring that calls and returns, ordered chronologically, are... well-bracketed. This is of course very natural, though restricted to sequential plays.

Secondly, in non-alternating games we have seen **logical well-bracketing** (Section 5.1.1), also used in concurrent games when constructing **$\rightarrow\dashv$-Strat** (Section 9.3.1). Logical well-bracketing asks that a function may only call its arguments *before* it returns, and may only return once all called arguments have returned. A logically well-bracketed play may not be chronologically well-bracketed even if alternating (Figure 5.3).

Next, in the definition of **NTCG** we have deployed *winning conditions* (Section 8.2.2) imported from [Melliès and Tabareau, 2007]. This **positional well-bracketing**, avoiding the explicit distinction of Questions and Answers, treats well-bracketing as a linearity constraint: a call may only be answered once. The *winning* mechanism enforces that winning strategies are never the first to break this linearity constraint, which hits surprisingly close to chronological well-bracketing at least for sequential innocent total strategies. In general, positional well-bracketing does not subsume the other more interactive notions, and *e.g.* cannot guarantee finite definability result. On the other hand, it is by far the best way to formulate the relational collapse of Section 10.4.

Finally, we have seen *globularity*, which is a **causal well-bracketing**: it ensures that the forking of merging of threads also respects the call/return discipline for parallel innocent strategies, in that a strategy may not merge threads with calls still pending since their fork. Again this is not guaranteed by our previous notions, bit is nevertheless required for the definability result of Chapter 12.

This profusion of subtly different notions of well-bracketing is messy and unsatisfactory. It feels that they could be unified in principle, but at the cost of requiring importing even more intensional information onto strategies, such as the *concurrency pointers* of [Laird, 2001b] to distinguish causal links coming from the term structure from those going through side-channel communication – this may allow us to extend causal well-bracketing beyond parallel innocent strategies. But does this actually work? And is it worth making the model even more complex? We leave this as an exercise to the reader.

### 14.2.4 Observing causality

Typically, concurrent games models are not fully abstract; as argued in Section 1.6 the strength of concurrent games is not to capture observational equivalence, but to record intensional information. Nevertheless, it is natural to wonder under which circumstances this causal information might be observed. From full abstraction results such as Theorem 5.1.12, this seems to boil down to asking when causal strategies may be entirely recovered (up to positive iso) from their non-alternating plays.
As presented in Section 13.1.1, the causal information *cannot* be reconstructed from plays in general. But we think it might be under the right circumstances: if each move can be replicated and the strategy is parallel innocent, then in principle causality may be observed by duplicating Opponent moves and observing the triggered duplications of Player moves. Indeed in examples, it is usually easy to define plays that separate distinct parallel innocent strategies. This brings us to the conjecture:

**Conjecture 14.2.4.** Consider A a mixed board such that no moves are answers, and $\sigma, \tau$: A two (possibly finite) parallel innocent strategies.

If $\mathcal{O}-\text{Unf}(\sigma) = \mathcal{O}-\text{Unf}(\tau)$, then $\sigma \approx \tau$.

If this was the case, it would likely entail that two terms in $\text{PCF}_{\parallel}$ yield isomorphic strategies if and only if they cannot be distinguished by contexts from $\text{IA}_{\parallel}$ extended with a control operator. However, one should not underestimate this problem: given a non-alternating play $s$, there may in principle be several parts of the strategy causing it – thus it is hard to pin down what one individual play teaches us about a strategy.

Perhaps the right path to that conjecture is via another:

**Conjecture 14.2.5.** Consider A a mixed board such that no moves are answers, and $\sigma, \tau$: A two (possibly finite) parallel innocent strategies.

If $(\sigma) = (\tau)$, then $\sigma \approx \tau$.

In [Blondeau-Patissier and Clairambault, 2021], we have already proved this for finite sequential innocent strategies. It would imply Conjecture 14.2.4, since the relational collapse can be extracted from the plays. The proof method for the sequential innocent case seems to extend in principle, but it becomes very technical and so far we have not managed to work out the details.

## 14.3 Perspectives and Future Directions

While the open problems above may tie loose ends and offer good avenues for short-term technical developments, they do not give long-term overarching research directions for the future. While we believe that the work reported here gives valuable steps in the direction presented in our introduction, the long-term goal is to use concurrent games to help make denotational semantics a connected mathematical theory. This suggests a *wealth* of research directions for the future, and we now introduce some of them.

**The cube of branching structure.** The core contribution of this monograph is the *disentangling of parallelism and state*, leading to a semantic square in the style of that presented in Section 3.3.3. This fits together parallelism and state in a single model, but why only those? After all, there are multiple other programming features studied in the game semantics literature – to cite only a few: control operators, exceptions, higher-order references, coroutines, probabilistic choice, etc. In principle, all of those semantics could be reformulated within concurrent games, but it does not seem such a good research strategy to do it exhaustively for all of them – if only because such a massive undertaking would prevent us from investigating other interesting questions.
<figure><img src="image_251.png" /><figcaption>Figure 14.2: The cube of branching structures</figcaption></figure>

So we introduce the following criterion. Some of the features above change the rules
following which control flows through the program, but do not change the *geometry* of
the control flow – this includes control operators, exceptions, higher-order references
and coroutines: adding any of those to a sequential deterministic programming language
yields a sequential deterministic programming language.

In contrast, some programming features heavily affect the geometric shape of execution: in this monograph, we have investigated in depth *parallelism*, and also *non-determinism* arising from the combination of parallelism and state. *Non-determinism* makes execution a tree, *parallelism* makes it a partial order, and the two together turn execution into an *event structure*. This makes concurrent games based on event structures perfect for this combination; we argue it is their ability to represent explicitly this *branching structure* that made possible the results presented in Part III. We expect giving a proper treatment of a new branching structure is a more fundamental problem than dealing with other programming features: after all, most of the non-branching effects mentioned above did *not* require changing much of the basic sequential deterministic game semantics canvas; unlike the results presented in this monograph.

There is a major branching structure that is not properly covered within this mono-
graph: *probabilistic choice*. By itself, it differs from non-deterministic choice by the ad-
dition of quantitative weights representing probabilities (as described in Section 13.2).
But more fundamentally, it is the branching structure in the presence of all three of par-
allelism, non-determinism and probabilistic choice that poses the real challenge. This
combination of branching effects is embodied by the cube in Figure 14.2.

Its left hand face is that studied in Part III. Its front face seems easy to handle working
from the results of Section 13.2. The real challenge is in dealing with the all three effects
together, which requires us to elaborate concurrent strategies to deal with the combina-
tion of non-determinism and probabilistic choice – perhaps based on de Visme's *mixed
event structures* [de Visme, 2019]. But besides having to develop a new theory of con-
current games, constructing a semantic cube to match Figure 14.2 means we *must* solve the open problems of Section 14.2.1 and give proper notions of probabilistic and non-deterministic parallel innocence. So this is a long-term objective that will require many developments before we can properly tackle it.

**Call-by-value and evaluation order.** A major element missing from all the development presented in this monograph, is evaluation order. All the languages considered here are call-by-name. This is mainly for historical reasons, because we connect to earlier work in the literature which is set in call-by-name. There is no obstacle, in principle, to replaying the results presented here in call-by-value: in particular, it has been known for a long time how to build games models for call-by-value languages [Abramsky and McCusker, 1997, Honda and Yoshida, 1999]. Our point here is not to redo all the previous work in call-by-value, as this would be a major undertaking offering comparatively little conceptual insight – though some of it does need to be redone.

There are several frameworks for languages and models encompassing both call-by-name and call-by-value: the main example is of course Levy's call-by-push-value [Levy, 1999] which focuses on the impact of evaluation order on effects, but also others such as the *bang calculus* (inspired from Girard's translations of intuitionistic logic into linear logic), which instead captures evaluation order via its impact on resource consumption [Ehrhard and Guerrieri, 2016]. Or finally, system L [Curien et al., 2016], encompassing both. This latter system, to our knowledge, does not yet have a concrete games model, which is unfortunate since it is the family of models that gives a concrete account of both effects and resources. A concurrent games analysis of such systems could be enlightening and also help us understand how *parallelism* fits into this picture.

In fact, there is currently increasing research activity revisiting classical topics (such as the pure $\lambda$-calculus, solvability, Böhm trees etc) in call-by-value. It seems that adequate notions of infinite normal forms in call-by-value include permutative equiva-lences inducing the structure of a DAG, rather than simply a tree [Accattoli et al., 2023], meaning that it might naturally yield a parallel innocent concurrent strategy. A natu-ral question is that of full abstraction for the pure $\lambda$-calculus in call-by-value, which is still missing; drawing inspirations from the results of this monograph this also of-fers enticing areas of investigation, connecting concurrent games with Taylor expansion [Kerinec et al., 2020] and intersection types [Arrial et al., 2023] in call-by-value.

Finally, a major objective is to extend our geometry of interaction multi-token ma-chine presented in Section 13.5 to a call-by-value language – this is a prerequisite before we can seriously investigate if it might be useful in practice. We have preliminary ideas about how such a machine should work exploiting subtle memoization mechanisms in Petri nets, but much ground work is needed: in call-by-name, the validity of the ma-chine rests on the adequate concurrent games model of $IA_\llcorner$ presented in Chapter 9, and no such model exists yet for a higher-order call-by-value stateful concurrent language.

**Taylor expansion and intersection types.** As reported in Section 13.4.3, for the pure $\lambda$-calculus, concurrent games offer a representation of programs very close to that proposed by the Taylor expansion of $\lambda$-terms [Ehrhard and Regnier, 2008] – more pre-
cisely, concurrent strategies form what could be regarded as a very rigid Taylor expan-
sion. With respect to game semantics, the Taylor expansion of $\lambda$-terms has the advan-
tage of being a syntactic method. This makes it much easier to deploy, and with a much
tighter connection with the original syntax. In return, concurrent games are much more
general, supporting with in the same framework many additional programming features
including non-determinism, concurrency, probabilistic choice, shared memory, etc.

This suggests a number of natural questions: to what extent could concurrent games
models be presented syntactically beyond the pure $\lambda$-calculus? How does it compare
with existing extensions of the Taylor expansion, such as for non-deterministic choice
[Olimpieri and Vaux Auclair, 2022] or probabilistic choice [Dal Lago and Leventis, 2019]?
Can we use concurrent games as a guide to construct intersection type systems or Tay-
lor expansions for effectful languages (such as IA$_{\emptyset}$), giving us the expressiveness of
concurrent games models without all the accompanying technical complications?

**Categorification.** Games models lack uniformity; while they often formalize sim-
ilar ideas and follow a common methodology, different models usually rest on very
different technical underpinnings. The work presented in this monograph attempts
to cope with this state of affairs by linking the models together, providing functo-
rial bridges that make explicit how they relate to concurrent games. But a comple-
mentary methodology is to capture the construction of various games models as in-
stances of one common categorical construction; notable works in this direction in-
clude [Eberhart and Hirschowitz, 2018] and more recently, Melliès' *template games*
[Melliès, 2019a, Melliès, 2019b]. However, for the time being, concurrent games evade
this categorical unification. Melliès' original template games lack mechanisms to elim-
inate deadlocking synchronizations – a new, more elaborate version [Melliès, 2021]
does capture the *interaction* of concurrent strategies (see Proposition 6.2.13), but not
the composition, for subtle reasons. So the question remains open: how should template
games be generalized so as to encompass concurrent games?

A strongly related topic is the proper categorical treatment of *symmetries* in con-
current games. Recently [Clairambault and Forest, 2023], we constructed a cartesian
closed bicategory of certain *spans of groupoids*, reproducing categorically much of the
structure of symmetries in thin concurrent games (but, like template games, also failing
to account for deadlocks in compositions). It is our conviction that a proper categorifi-
cation of game semantics should rest on thin spans of groupoids. The link with template
games is fascinating, as the two models use completely different mechanisms to account
for replication of resources – thin spans are *thin* as in thin concurrent games, while tem-
plate games are *saturated* (as in Section 7.1.2). Another fundamental question is the
link with distributors and generalized species of structure; we give some elements in
[Clairambault et al., 2023b] but this should be completed to account for inclusion of
configurations and not just symmetries, and should also include a proper treatment of
the linear bicategorical (or double-categorical) structure.

Thin spans of groupoids really are *thin concurrent games without concurrent games*.
It seems that many of our passed achievements with thin concurrent games (typically,
the enrichment with quantitative valuations and the corresponding relational collapses,
up to generalized species of structure) are actually independent from the basic game
mechanisms, and should really be carried out in thin spans of groupoids instead. We
should spell this out and investigate extensions made possible by the fact that we are no
longer hindered by the intricate combinatorics of strategy composition.

**Qualitative concurrent games.** Thin concurrent games are a *quantitative* model, in the sense that they record explicitly the *multiplicity* of resource usage – even more, each individual move has a separate identity, formalized as a copy index. In categorified relational models such as distributors, it is possible to change the exponential modality to make it *qualitative*; this is done by changing the *morphisms* in !A so as to allow contraction and weakening. In principle, the same could be done in thin concurrent games, by generalizing *symmetries* to encompass more general relations between configurations that may not preserve multiplicity. There are fundamental questions to solve regarding how such relations behave with respect to polarity. A first concrete objective would be to construct such a generalization of thin concurrent games, and deduce a new, more concrete proof of Ehrhard’s *extensional collapse theorem* [Ehrhard, 2012] linking qualitative and quantitative models.

One interest of such a concrete proof is that we expect it to generalize in a situ-
ation with *infinite multiplicities*. More precisely, we aim to generalize the relational
collapse presented in this monograph to a collapse to the *infinitary relational model*
[Grellois and Melliès, 2015], also accounting for infinite configurations. Paired with an
infinitary version of Ehrhard’s extensional collapse, we expect this is the key ingredient
to a purely semantic proof of the decidability of the higher-order model-checking prob-
lem, which would be a beautiful illustration of the strength of thin concurrent games.
Bibliography

[Abramsky, 2003] Abramsky, S. (2003). Sequentiality vs. concurrency in games and logic. *Math. Struct. Comput. Sci.*, 13(4):531–565.

[Abramsky et al., 1998] Abramsky, S., Honda, K., and McCusker, G. (1998). A fully abstract game semantics for general references. In *Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998*, pages 334–344. IEEE Computer Society.

[Abramsky et al., 2000] Abramsky, S., Jagadeesan, R., and Malacaria, P. (2000). Full abstraction for PCF. *Inf. Comput.*, 163(2):409–470.

[Abramsky and McCusker, 1996] Abramsky, S. and McCusker, G. (1996). Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. *Electron. Notes Theor. Comput. Sci.*, 3:2–14.

[Abramsky and McCusker, 1997] Abramsky, S. and McCusker, G. (1997). Call-by-value games. In *CSL*, volume 1414 of *Lecture Notes in Computer Science*, pages 1–17. Springer.

[Abramsky and Melliès, 1999] Abramsky, S. and Melliès, P. (1999). Concurrent games and full completeness. In *LICS*, pages 431–442. IEEE Computer Society.

[Accattoli et al., 2023] Accattoli, B., Faggian, C., and Lancelot, A. (2023). Normal form bisimulations by value. *CoRR*, abs/2303.08161.

[Alcolei et al., 2018] Alcolei, A., Clairambault, P., Hyland, M., and Winskel, G. (2018). The true concurrency of herbrand's theorem. In *CSL*, volume 119 of *LIPIcs*, pages 5:1–5:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[Alcolei et al., 2019] Alcolei, A., Clairambault, P., and Laurent, O. (2019). Resource-tracking concurrent games. In *FoSSaCS*, volume 11425 of *Lecture Notes in Computer Science*, pages 27–44. Springer.

[Altenkirch et al., 2010] Altenkirch, T., Chapman, J., and Uustalu, T. (2010). Monads need not be endofunctors. In *International Conference on Foundations of Software Science and Computational Structures*, pages 297–311. Springer.

[Arnold and Niwiński, 2001] Arnold, A. and Niwiński, D. (2001). *Rudiments of μ-calculus*. Elsevier.
[Arrial et al., 2023] Arrial, V., Guerrieri, G., and Kesner, D. (2023). Quantitative in-habitation for different lambda calculi in a unifying framework. *Proc. ACM Program. Lang.*, 7(POPL):1483–1513.

[Baillot, 1999] Baillot, P. (1999). *Approches dynamiques en sémantique de la logique linéaire: jeux et géométrie de l'interaction*. PhD thesis, Aix-Marseille 2.

[Baillot et al., 1997a] Baillot, P., Danos, V., Ehrhard, T., and Regnier, L. (1997a). Believe it or not, ajm's games model is a model of classical linear logic. In *LICS*, pages 68–75. IEEE Computer Society.

[Baillot et al., 1997b] Baillot, P., Danos, V., Ehrhard, T., and Regnier, L. (1997b). Timeless games. In *Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers*, pages 56–77.

[Blass, 1992] Blass, A. (1992). A game semantics for linear logic. *Ann. Pure Appl. Log.*, 56(1-3):183–220.

[Blondeau-Patissier and Clairambault, 2021] Blondeau-Patissier, L. and Clairambault, P. (2021). Positional injectivity for innocent strategies. In Kobayashi, N., editor, *6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)*, volume 195 of *LIPIcs*, pages 17:1–17:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[Blondeau-Patissier et al., 2023a] Blondeau-Patissier, L., Clairambault, P., and Vaux Auclair, L. (2023a). Extensional taylor expansion. *CoRR*, abs/2305.08489.

[Blondeau-Patissier et al., 2023b] Blondeau-Patissier, L., Clairambault, P., and Vaux Auclair, L. (2023b). Strategies as resource terms, and their categorical semantics. In Gaboardi, M. and van Raamsdonk, F., editors, *8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy*, volume 260 of *LIPIcs*, pages 13:1–13:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[Blute et al., 2020] Blute, R., Cockett, J. R. B., Lemay, J. P., and Seely, R. A. G. (2020). Differential categories revisited. *Appl. Categorical Struct.*, 28(2):171–235.

[Boudes, 2009] Boudes, P. (2009). Thick subtrees, games and experiments. In *Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings*, pages 65–79.

[Calderon and McCusker, 2010] Calderon, A. C. and McCusker, G. (2010). Understanding game semantics through coherence spaces. *Electr. Notes Theor. Comput. Sci.*, 265:231–244.

[Cartwright et al., 1994] Cartwright, R., Curien, P., and Felleisen, M. (1994). Fully abstract semantics for observably sequential languages. *Inf. Comput.*, 111(2):297–401.
[Castellan, 2015] Castellan, S. (2015). La stratégie de la fourchette. In *Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015)*.

[Castellan and Clairambault, 2016] Castellan, S. and Clairambault, P. (2016). Causal-ity vs. interleavings in concurrent game semantics. In *CONCUR*, volume 59 of *LIPIcs*, pages 32:1–32:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[Castellan and Clairambault, 2021] Castellan, S. and Clairambault, P. (2021). Disentangling parallelism and interference in game semantics. Submitted.

[Castellan and Clairambault, 2023] Castellan, S. and Clairambault, P. (2023). The geometry of causality: Multi-token geometry of interaction and its causal unfolding. *Proc. ACM Program. Lang.*, 7(POPL):689–717.

[Castellan et al., 2018a] Castellan, S., Clairambault, P., Hayman, J., and Winskel, G. (2018a). Non-angelic concurrent game semantics. In Baier, C. and Lago, U. D., editors, *Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings*, volume 10803 of *Lecture Notes in Computer Science*, pages 3–19. Springer.

[Castellan et al., 2018b] Castellan, S., Clairambault, P., Paquet, H., and Winskel, G. (2018b). The concurrent game semantics of probabilistic PCF. In *LICS*, pages 215–224. ACM.

[Castellan et al., 2017a] Castellan, S., Clairambault, P., Rideau, S., and Winskel, G. (2017a). Games and strategies as event structures. *Log. Methods Comput. Sci.*, 13(3).

[Castellan et al., 2014] Castellan, S., Clairambault, P., and Winskel, G. (2014). Symmetry in concurrent games. In Henzinger, T. A. and Miller, D., editors, *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 28:1–28:10. ACM.

[Castellan et al., 2015] Castellan, S., Clairambault, P., and Winskel, G. (2015). The parallel intensionally fully abstract games model of PCF. In *30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015*, pages 232–243. IEEE Computer Society.

[Castellan et al., 2017b] Castellan, S., Clairambault, P., and Winskel, G. (2017b). Observably deterministic concurrent strategies and intensional full abstraction for parallel-or. In *FSCD*, volume 84 of *LIPIcs*, pages 12:1–12:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[Castellan et al., 2019] Castellan, S., Clairambault, P., and Winskel, G. (2019). Thin games with symmetry and concurrent hyland-ong games. *Log. Methods Comput. Sci.*, 15(1).
[Chappe et al., 2023] Chappe, N., He, P., Henrio, L., Zakowski, Y., and Zdancewic, S. (2023). Choice trees: Representing nondeterministic, recursive, and impure programs in coq. *Proc. ACM Program. Lang.*, 7(POPL):1770–1800.

[Clairambault, 2010] Clairambault, P. (2010). *Logique et Interaction : une Étude Sé-mantique de la Totalité. (Logic and Interaction : a Semantic Study of Totality)*. PhD thesis, Paris Diderot University, France.

[Clairambault, 2023] Clairambault, P. (2023). A tale of additives and concurrency in game semantics. In *Samson Abramsky on Logic and Structure in Computer Science and Beyond*, pages 363–414. Springer.

[Clairambault and de Visme, 2020] Clairambault, P. and de Visme, M. (2020). Full abstraction for the quantum lambda-calculus. *Proc. ACM Program. Lang.*, 4(POPL):63:1–63:28.

[Clairambault et al., 2019] Clairambault, P., de Visme, M., and Winskel, G. (2019). Game semantics for quantum programming. *Proc. ACM Program. Lang.*, 3(POPL):32:1–32:29.

[Clairambault and Forest, 2023] Clairambault, P. and Forest, S. (2023). The cartesian closed bicategory of thin spans of groupoids. In *LICS*, pages 1–13.

[Clairambault et al., 2012] Clairambault, P., Gutierrez, J., and Winskel, G. (2012). The winning ways of concurrent games. In *LICS*, pages 235–244. IEEE Computer Society.

[Clairambault and Harmer, 2010] Clairambault, P. and Harmer, R. (2010). Totality in arena games. *Ann. Pure Appl. Logic*, 161(5):673–689.

[Clairambault et al., 2023a] Clairambault, P., Olimpieri, F., and Paquet, H. (2023a). From thin concurrent games to generalized species of structure. In *Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, US, June 26–29, 2023*. To appear.

[Clairambault et al., 2023b] Clairambault, P., Olimpieri, F., and Paquet, H. (2023b). From thin concurrent games to generalized species of structures. In *LICS*, pages 1–14.

[Clairambault and Paquet, 2021] Clairambault, P. and Paquet, H. (2021). The quantitative collapse of concurrent games with symmetry. *CoRR*, abs/2107.03155.

[Coquand, 1995] Coquand, T. (1995). A semantics of evidence for classical arithmetic. *J. Symb. Log.*, 60(1):325–337.

[Curien and Faggian, 2005] Curien, P. and Faggian, C. (2005). L-nets, strategies and proof-nets. In *CSL, volume 3634 of Lecture Notes in Computer Science*, pages 167–183. Springer.

[Curien et al., 2016] Curien, P., Fiore, M. P., and Munch-Maccagnoni, G. (2016). A theory of effects and resources: adjunction models and polarised calculi. In *POPL*, pages 44–56. ACM.
[Dal Lago and Leventis, 2019] Dal Lago, U. and Leventis, T. (2019). On the taylor expansion of probabilistic lambda-terms. In Geuvers, H., editor, *4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany*, volume 131 of LIPIcs, pages 13:1–13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[Danos and Ehrhard, 2011] Danos, V. and Ehrhard, T. (2011). Probabilistic coherence spaces as a model of higher-order probabilistic computation. *Inf. Comput.*, 209(6):966–991.

[Danos and Harmer, 2000] Danos, V. and Harmer, R. (2000). Probabilistic game semantics. In *LICS*, pages 204–213. IEEE Computer Society.

[Danos et al., 1996] Danos, V., Herbelin, H., and Regnier, L. (1996). Game semantics & abstract machines. In *Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996*, pages 394–405. IEEE Computer Society.

[Danos and Regnier, 1996] Danos, V. and Regnier, L. (1996). Reversible, irreversible and optimal lambda-machines. In *Linear Logic Tokyo Meeting*, volume 3 of *Electronic Notes in Theoretical Computer Science*, pages 40–60. Elsevier.

[de Carvalho and de Falco, 2012] de Carvalho, D. and de Falco, L. T. (2012). The relational model is injective for multiplicative exponential linear logic (without weakenings). *Ann. Pure Appl. Log.*, 163(9):1210–1236.

[de Visme, 2019] de Visme, M. (2019). Event structures for mixed choice. In Fokkink, W. J. and van Glabbeek, R., editors, *30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands*, volume 140 of LIPIcs, pages 11:1–11:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

[Dixon et al., 2021a] Dixon, A., Lazic, R., Murawski, A. S., and Walukiewicz, I. (2021a). Leafy automata for higher-order concurrency. In *FoSSaCS*, volume 12650 of Lecture Notes in Computer Science, pages 184–204. Springer.

[Dixon et al., 2021b] Dixon, A., Lazic, R., Murawski, A. S., and Walukiewicz, I. (2021b). Verifying higher-order concurrency with data automata. In *LICS*, pages 1–13. IEEE.

[Eberhart and Hirschowitz, 2018] Eberhart, C. and Hirschowitz, T. (2018). What's in a game?: A theory of game models. In Dawar, A. and Grädel, E., editors, *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018*, pages 374–383. ACM.

[Eberhart et al., 2017] Eberhart, C., Hirschowitz, T., and Seiller, T. (2017). An intentionally fully-abstract sheaf model for $\pi$ (expanded version). *Log. Methods Comput. Sci.*, 13(4).

[Ehrhard, 2012] Ehrhard, T. (2012). The scott model of linear logic is the extensional collapse of its relational model. *Theor. Comput. Sci.*, 424:20–45.
[Ehrhard and Guerrieri, 2016] Ehrhard, T. and Guerrieri, G. (2016). The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In *PPDP*, pages 174–187. ACM.

[Ehrhard et al., 2018] Ehrhard, T., Pagani, M., and Tasson, C. (2018). Full abstraction for probabilistic PCF. *J. ACM*, 65(4):23:1–23:44.

[Ehrhard and Regnier, 2003] Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. *Theor. Comput. Sci.*, 309(1-3):1–41.

[Ehrhard and Regnier, 2008] Ehrhard, T. and Regnier, L. (2008). Uniformity and the taylor expansion of ordinary lambda-terms. *Theor. Comput. Sci.*, 403(2-3):347–372.

[Faggian and Hyland, 2002] Faggian, C. and Hyland, M. (2002). Designs, disputes and strategies. In *CSL*, volume 2471 of *Lecture Notes in Computer Science*, pages 442–457. Springer.

[Faggian and Maurel, 2005] Faggian, C. and Maurel, F. (2005). Ludics nets, a game model of concurrent interaction. In *LICS*, pages 376–385. IEEE Computer Society.

[Faggian and Piccolo, 2009] Faggian, C. and Piccolo, M. (2009). Partial orders, event structures and linear strategies. In *TLCA*, volume 5608 of *Lecture Notes in Computer Science*, pages 95–111. Springer.

[Fiore et al., 2008] Fiore, M., Gambino, N., Hyland, M., and Winskel, G. (2008). The cartesian closed bicategory of generalised species of structures. *Journal of the London Mathematical Society*, 77(1):203–220.

[Gabbay and Ghica, 2012] Gabbay, M. and Ghica, D. R. (2012). Game semantics in the nominal model. In *MFPS*, volume 286 of *Electronic Notes in Theoretical Computer Science*, pages 173–189. Elsevier.

[Ghica, 2005] Ghica, D. R. (2005). Slot games: a quantitative model of computation. In Palsberg, J. and Abadi, M., editors, *Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005*, Long Beach, California, USA, January 12-14, 2005, pages 85–97. ACM.

[Ghica and McCusker, 2003] Ghica, D. R. and McCusker, G. (2003). The regular-language semantics of second-order idealized Algol. *Theor. Comput. Sci.*, 309(1-3):469–502.

[Ghica and Murawski, 2004] Ghica, D. R. and Murawski, A. S. (2004). Angelic semantics of fine-grained concurrency. In *FoSSaCS*, volume 2987 of *Lecture Notes in Computer Science*, pages 211–225. Springer.

[Ghica and Murawski, 2008] Ghica, D. R. and Murawski, A. S. (2008). Angelic semantics of fine-grained concurrency. *Ann. Pure Appl. Log.*, 151(2-3):89–114.

[Ghica et al., 2006] Ghica, D. R., Murawski, A. S., and Ong, C. L. (2006). Syntactic control of concurrency. *Theor. Comput. Sci.*, 350(2-3):234–251.

[Ghica and Tzevelekos, 2012] Ghica, D. R. and Tzevelekos, N. (2012). A system-level game semantics. In Berger, U. and Mislove, M. W., editors, *Proceedings of the 28th*
*Conference on the Mathematical Foundations of Programming Semantics, MFPS 2012, Bath, UK, June 6-9, 2012, volume 286 of Electronic Notes in Theoretical Computer Science*, pages 191–211. Elsevier.

[Girard, 1987] Girard, J. (1987). Linear logic. *Theor. Comput. Sci.*, 50:1–102.

[Girard, 1988] Girard, J. (1988). Normal functors, power series and λ-calculus. *Ann. Pure Appl. Log.*, 37(2):129–177.

[Girard, 2001] Girard, J. (2001). Locus solum: From the rules of logic to the logic of rules. *Math. Struct. Comput. Sci.*, 11(3):301–506.

[Girard, 1989] Girard, J.-Y. (1989). Geometry of Interaction 1: Interpretation of System F. In *Studies in Logic and the Foundations of Mathematics*, volume 127, pages 221–260. Elsevier.

[Goyet, 2013] Goyet, A. (2013). The lambda lambda-bar calculus: a dual calculus for unconstrained strategies. In *POPL*, pages 155–166. ACM.

[Grellois and Melliès, 2015] Grellois, C. and Melliès, P. (2015). An infinitary model of linear logic. In Pitts, A. M., editor, *Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings*, volume 9034 of *Lecture Notes in Computer Science*, pages 41–55. Springer.

[Griffin, 1990] Griffin, T. (1990). A formulae-as-types notion of control. In Allen, F. E., editor, *Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990*, pages 47–58. ACM Press.

[Harmer, 1999] Harmer, R. (1999). *Games and full abstraction for non-deterministic languages*. PhD thesis, Imperial College London, UK.

[Harmer, 2004] Harmer, R. (2004). Innocent game semantics. *Lecture notes*, 2007.

[Harmer et al., 2007] Harmer, R., Hyland, M., and Melliès, P. (2007). Categorical combinatorics for innocent strategies. In *LICS*, pages 379–388. IEEE Computer Society.

[Harmer and McCusker, 1999] Harmer, R. and McCusker, G. (1999). A fully abstract game semantics for finite nondeterminism. In *14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999*, pages 422–430. IEEE Computer Society.

[Honda and Yoshida, 1999] Honda, K. and Yoshida, N. (1999). Game-theoretic analysis of call-by-value computation. *Theor. Comput. Sci.*, 221(1-2):393–456.

[Hyland and Ong, 2000] Hyland, J. M. E. and Ong, C. L. (2000). On full abstraction for PCF: I, II, and III. *Inf. Comput.*, 163(2):285–408.

[Hyland, 1997] Hyland, M. (1997). Game semantics. *Semantics and Logics of Computation*, 14:131.
[Hyland and Schalk, 2002] Hyland, M. and Schalk, A. (2002). Games on graphs and sequentially realizable functionals. In *17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings*, pages 257-264. IEEE Computer Society.

[Jaber, 2015] Jaber, G. (2015). Operational nominal game semantics. In Pitts, A. M., editor, *Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015*. *Proceedings*, volume 9034 of *Lecture Notes in Computer Science*, pages 264-278. Springer.

[Jacq and Melliès, 2018] Jacq, C. and Melliès, P. (2018). Categorical combinatorics for non deterministic strategies on simple games. In Baier, C. and Lago, U. D., editors, *Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings*, volume 10803 of *Lecture Notes in Computer Science*, pages 39-70. Springer.

[Joyal, 1977] Joyal, A. (1977). Remarques sur la théorie des jeux à deux personnes. *Gazette des sciences mathématiques du Québec*, 1(4):46-52.

[Kelly and Laplaza, 1980] Kelly, G. M. and Laplaza, M. L. (1980). Coherence for compact closed categories. *Journal of pure and applied algebra*, 19:193-213.

[Ker et al., 2002] Ker, A. D., Nickau, H., and Ong, C. L. (2002). Innocent game models of untyped lambda-calculus. *Theor. Comput. Sci.*, 272(1-2):247-292.

[Kerinec et al., 2020] Kerinec, A., Manzonetto, G., and Pagani, M. (2020). Revisiting call-by-value böhm trees in light of their taylor expansion. *Log. Methods Comput. Sci.*, 16(3).

[Koenig and Shao, 2020] Koenig, J. and Shao, Z. (2020). Refinement-based game semantics for certified abstraction layers. In *LICS*, pages 633-647. ACM.

[Krebbers et al., 2014] Krebbers, R., Leroy, X., and Wiedijk, F. (2014). Formal C semantics: Compcert and the C standard. In Klein, G. and Gamboa, R., editors, *Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings*, volume 8558 of *Lecture Notes in Computer Science*, pages 543-548. Springer.

[Laird, 1997] Laird, J. (1997). Full abstraction for functional languages with control. In *LICS*, pages 58-67. IEEE Computer Society.

[Laird, 2001a] Laird, J. (2001a). A fully abstract game semantics of local exceptions. In *LICS*, pages 105-114. IEEE Computer Society.

[Laird, 2001b] Laird, J. (2001b). A game semantics of idealized CSP. In *MFPS*, volume 45 of *Electronic Notes in Theoretical Computer Science*, pages 232-257. Elsevier.
[Laird, 2002] Laird, J. (2002). A categorical semantics of higher order store. In *CTCS*, volume 69 of *Electronic Notes in Theoretical Computer Science*, pages 209–226. Elsevier.

[Laird, 2007] Laird, J. (2007). A fully abstract trace semantics for general references. In *ICALP*, volume 4596 of *Lecture Notes in Computer Science*, pages 667–679. Springer.

[Laird et al., 2013] Laird, J., Manzonetto, G., McCusker, G., and Pagani, M. (2013). Weighted relational models of typed lambda-calculi. In *LICS*, pages 301–310. IEEE Computer Society.

[Lambek and Scott, 1988] Lambek, J. and Scott, P. J. (1988). *Introduction to higher-order categorical logic*, volume 7. Cambridge University Press.

[Laurent, 2002] Laurent, O. (2002). Polarized games. In *LICS*, page 265. IEEE Computer Society.

[Leroy, 2009] Leroy, X. (2009). Formal verification of a realistic compiler. *Commun. ACM*, 52(7):107–115.

[Levy, 1999] Levy, P. B. (1999). Call-by-push-value: A subsuming paradigm. In *TLCA*, volume 1581 of *Lecture Notes in Computer Science*, pages 228–242. Springer.

[Levy, 2014] Levy, P. B. (2014). Transition systems over games. Talk at the *Chocola* seminar.

[Levy and Staton, 2014] Levy, P. B. and Staton, S. (2014). Transition systems over games. In *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 64:1–64:10.

[Loader, 2001] Loader, R. (2001). Finitary PCF is not decidable. *Theor. Comput. Sci.*, 266(1-2):341–364.

[Mackie, 1995] Mackie, I. (1995). The geometry of interaction machine. In *POPL*, pages 198–208. ACM Press.

[McCusker, 2003] McCusker, G. (2003). On the semantics of the bad-variable constructor in algol-like languages. In *MFPS*, volume 83 of *Electronic Notes in Theoretical Computer Science*, pages 169–186. Elsevier.

[Melliès, 2004a] Melliès, P. (2004a). Asynchronous games 2: The true concurrency of innocence. In *CONCUR*, volume 3170 of *Lecture Notes in Computer Science*, pages 448–465. Springer.

[Melliès, 2004b] Melliès, P. (2004b). Asynchronous games 3 an innocent model of linear logic. In *CTCS*, volume 122 of *Electronic Notes in Theoretical Computer Science*, pages 171–192. Elsevier.

[Melliès, 2005] Melliès, P. (2005). Asynchronous games 4: A fully complete model of propositional linear logic. In *LICS*, pages 386–395. IEEE Computer Society.
[Melliès, 2006] Melliès, P. (2006). Asynchronous games 2: The true concurrency of innocence. *Theor. Comput. Sci.*, 358(2-3):200–228.

[Melliès, 2019a] Melliès, P. (2019a). Categorical combinatorics of scheduling and synchronization in game semantics. *Proc. ACM Program. Lang., 3(POPL):23:1–23:30.*

[Melliès, 2019b] Melliès, P. (2019b). Template games and differential linear logic. In *34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019*, pages 1–13. IEEE.

[Melliès, 2021] Melliès, P. (2021). Asynchronous template games and the gray tensor product of 2-categories. In *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021*, pages 1–13. IEEE.

[Melliès and Mimram, 2007] Melliès, P. and Mimram, S. (2007). Asynchronous games: Innocence without alternation. In *CONCUR*, volume 4703 of *Lecture Notes in Computer Science*, pages 395–411. Springer.

[Melliès and Tabareau, 2007] Melliès, P. and Tabareau, N. (2007). Resource modalities in game semantics. In *LICS*, pages 389–398. IEEE Computer Society.

[Melliès, 2003] Melliès, P.-A. (2003). Asynchronous games 1: Uniformity by group invariance.

[Melliès, 2009] Melliès, P.-A. (2009). Categorical semantics of linear logic. *Panoramas et synthèses*, 27:15–215.

[Miller, 1987] Miller, D. A. (1987). A compact representation of proofs. *Stud Logica*, 46(4):347–370.

[Mimram, 2008] Mimram, S. (2008). *Sémantique des jeux asynchrones et réécriture 2-dimensionnelle*. (Asynchronous Game Semantics and 2-dimensional Rewriting Systems). PhD thesis, Paris Diderot University, France.

[Moggi, 1991] Moggi, E. (1991). Notions of computation and monads. *Inf. Comput.*, 93(1):55–92.

[Murawski, 2007] Murawski, A. S. (2007). Bad variables under control. In *CSL*, volume 4646 of *Lecture Notes in Computer Science*, pages 558–572. Springer.

[Murawski, 2010] Murawski, A. S. (2010). Full abstraction without synchronization primitives. In *MFPS*, volume 265 of *Electronic Notes in Theoretical Computer Science*, pages 423–436. Elsevier.

[Murawski and Tzevelekos, 2013] Murawski, A. S. and Tzevelekos, N. (2013). Deconstructing general references via game semantics. In *FoSSaCS*, volume 7794 of *Lecture Notes in Computer Science*, pages 241–256. Springer.

[New et al., 2016] New, M. S., Bowman, W. J., and Ahmed, A. (2016). Fully abstract compilation via universal embedding. In *Garrigue, J.*, *Keller, G.*, and *Sumii, E.*, editors, *Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016*, pages 103–116. ACM.
ory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, volume 1243 of Lecture Notes in Computer Science, pages 376-390. Springer.

[Stewart et al., 2015] Stewart, G., Beringer, L., Cuellar, S., and Appel, A. W. (2015). Compositional compcert. In *POPL*, pages 275-287. ACM.

[Tsukada and Ong, 2015] Tsukada, T. and Ong, C. L. (2015). Nondeterminism in game semantics via sheaves. In *30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015*, pages 220-231. IEEE Computer Society.

[Tsukada and Ong, 2016] Tsukada, T. and Ong, C. L. (2016). Plays as resource terms via non-idempotent intersection types. In Grohe, M., Koskinen, E., and Shankar, N., editors, *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016*, pages 237-246. ACM.

[Turi and Plotkin, 1997] Turi, D. and Plotkin, G. D. (1997). Towards a mathematical operational semantics. In *LICS*, pages 280-291. IEEE Computer Society.

[Tzevelekos, 2009] Tzevelekos, N. (2009). Full abstraction for nominal general references. *Log. Methods Comput. Sci.*, 5(3).

[Vale et al., 2023] Vale, A. O., Shao, Z., and Chen, Y. (2023). A compositional theory of linearizability. *Proc. ACM Program. Lang.*, 7(POPL):1089-1120.

[Winskel, 1980] Winskel, G. (1980). *Events in computation*. PhD Thesis, Edinburgh University.

[Winskel, 1982] Winskel, G. (1982). Event structure semantics for CCS and related languages. In Nielsen, M. and Schmidt, E. M., editors, *Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings*, volume 140 of *Lecture Notes in Computer Science*, pages 561-576. Springer.

[Winskel, 1986] Winskel, G. (1986). Event structures. In Brauer, W., Reisig, W., and Rozenberg, G., editors, *Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986*, volume 255 of *Lecture Notes in Computer Science*, pages 325-392. Springer.

[Winskel, 1993] Winskel, G. (1993). *The formal semantics of programming languages: an introduction*. MIT press.

[Winskel, 2007] Winskel, G. (2007). Event structures with symmetry. *Electron. Notes Theor. Comput. Sci.*, 172:611-652.

[Winskel, 2013a] Winskel, G. (2013a). Distributed probabilistic and quantum strategies. In *MFPS*, volume 298 of *Electronic Notes in Theoretical Computer Science*, pages 403-425. Elsevier.

[Winskel, 2013b] Winskel, G. (2013b). Strategies as profunctors. In Pfenning, F., editor, *Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences*
on *Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings*, volume 7794 of *Lecture Notes in Computer Science*, pages 418–433. Springer.

[Xia et al., 2020] Xia, L., Zakowski, Y., He, P., Hur, C., Malecha, G., Pierce, B. C., and Zdancewic, S. (2020). Interaction trees: representing recursive and impure programs in coq. *Proc. ACM Program. Lang.*, 4(POPL):51:1–51:32.
# Part V

## Appendices
# Appendix A

## Complements on Relative Seely Categories

Like many other works in denotational semantics, the developments appearing in this monograph target programming languages with a non-linear type system, whose models are certain cartesian closed categories. But as is also common in denotational semantics, our cartesian closed categories are constructed following a linear decomposition, from a model of intuitionistic linear logic. A standard categorical structure used for this purpose is that of a *Seely category* [Melliès, 2009]: it is a symmetric monoidal closed category C also equipped with a cartesian structure along with a comonad ! on C and

$$!A \otimes !B \cong ! (A \& B), \qquad 1 \cong !T,$$

natural isos called the *Seely isomorphisms* satisfying a few coherence conditions.

It is possible to build a genuine Seely category of games and concurrent strategies, and this is done for instance in [Castellan and Clairambault, 2021]. But the construction is inelegant: as argued in Section 8.2, handling types such as $o \sim (o \otimes o)$ with a tensor on the right hand side complicates the shape of games and weakens the connection with the relational model. So we shall ban such types and work not with Seely categories, but with *relative* Seely categories, defined and developed here<fnref n="1" />.

In Section A.1, we first define relative Seely category, then construct the cartesian closed Kleisli category of a Seely category. Then, in Section A.2 we shall define functors between relative Seely categories, and show how they lift to the Kleisli category.

<footnote n="1">¹More precisely, the monograph builds on *relative Seely ~-category*, where every law holds up to an equivalence relation ~, which is also preserved by all constructions on morphisms – but we omit it in this appendix as it is completely orthogonal to the development.</footnote>
## A.1 Definition and Kleisli Category

**Definition.** It seems natural to first restate the definition from Section 8.2.1:

**Definition 8.2.1.** A relative Seely category is a symmetric monoidal category $(C, \otimes, 1)$ equipped with a full subcategory $C_s$ together with the following data and axioms:

* $C_s$ has finite products $(\& , \top)$ preserved by the inclusion functor $J : C_s \hookrightarrow C$.

* For every $B \in C$ there is a functor $B \to - : C_s \to C_s$, such that there is

$$ \Lambda(-) : C(A \otimes B, S) \cong C(A, B \to S). $$

a bijection natural in $A \in C$ and $S \in C_s$.

* There is a $J$-relative comonad $! : C_s \to C$ : we have, for every $S \in C_s$, an object $!S \in C$ and a dereliction morphism $\mathrm{der}_S : !S \to S$, and for every $\sigma : !S \to T$, a promotion $\sigma^1 : !S \to !T$, subject to three axioms [Altenkirch et al., 2010]:

$$ \mathrm{der}_T \circ \sigma^1 = \sigma \qquad (\sigma : !S \to T) $$

$$ \mathrm{der}_S^1 = \mathrm{id}_{S} \qquad (S \in C_s) $$

$$ (\tau \circ \sigma^1)^1 = \tau^1 \circ \sigma^1 \qquad (\sigma : !S \to T, \tau : T \to U), $$

which make $! : C_s \to C$ a functor, via $!\sigma = (\sigma \circ \mathrm{der}_S)^1$ for $\sigma : S \to T$.

* The functor $! : C_s \to C$ is symmetric strong monoidal $(C_s, \& , \top) \to (C, \otimes, 1)$, so

$$ m_0 : 1 \to !\top \qquad m_{S,T} : !S \otimes !T \to !(S\&T) $$

are natural isos, additional compatible with promotion: the diagram

<figure><img src="image_252.png" /></figure>

commutes for all $\Gamma, S, T \in C_s, f \in C(\Gamma, S), g \in C(\Gamma, T)$.

As we shall annotate with ! the components of the constructed Kleisli category, we prefer to write the promotion as $\sigma^\dagger$ from now on (rather than $\sigma^1$), to avoid the collision.

**Kleisli category.** We define the Kleisli category $C_1$ as follows. Its objects are simply those of $C_s$. A morphism from $S$ to $T$ is $f : !S \to T$ in $C$. The identity on object $S$ is $\mathrm{id}_S^\dagger = \mathrm{der}_S : !S \to S$. The composition of $\sigma \in C_1(S, T)$ and $\tau \in C_1(T, U)$ is

$$ \tau \circ \sigma^1 = \tau \circ \sigma^\dagger. $$

It is completely straightforward that this data defines a category; the equations to be verified directly boil down to the axioms of relative comonads above. Thus we have:

**Proposition A.1.1.** The data above forms a category $C_1$, the Kleisli category of !.
**Cartesian closed structure.** Obviously, $\mathbb{T}$ is still terminal in $C_1$. If $S, T \in C_s$, their product is $S \& T \in C_s$. The corresponding projections are (in $C$):

$$ 
\begin{aligned}
\pi_S^1 &= \pi_S \circ \operatorname{der}_{S \& T} : ! (S \& T) \to S \\
\pi_T^1 &= \pi_T \circ \operatorname{der}_{S \& T} : ! (S \& T) \to T,
\end{aligned}
$$

and the pairing of $\sigma : \mathbb{T} \to S$ and $\tau : \mathbb{T} \to T$ is $\langle \sigma, \tau \rangle_! = \langle \sigma, \tau \rangle$. It is easy to check:

**Proposition A.1.2.** *This data equips $C_1$ with a cartesian structure.*

Likewise, given $S, T \in C_s$, their arrow is $S \Rightarrow T = !S \dashv T$. The evaluation is

$$ \mathrm{ev}_{S,T} \quad = \quad !((!S \dashv T) \& S) \xrightarrow{m_{S \dashv T,S}^{-1}} !(!S \dashv T) \otimes !S \xrightarrow{\mathrm{der}_{S \dashv T} \otimes !S} (!S \dashv T) \otimes !S \xrightarrow{\mathrm{ev}_{S,T}} T $$

and given $\sigma : ! (S \& T) \to U$, its currying is $\Lambda_{S,T,U}^1 = \Lambda_{S,T,U} (\sigma \circ m_{S,T})$ which is in $C_1(S, !T \dashv U)$ as required. Again, it is an elementary verification that:

**Theorem A.1.3.** *This data equips $C_1$ with a cartesian closed structure.*

## A.2 Relative Seely Functors

Theorem A.1.3 is our main tool to construct cartesian closed categories in this monograph; but we also need an accompanying tool to construct cartesian closed functors from an appropriate notion of functor between relative Seely categories.

**Definition.** Let us start by defining relative Seely functors.

**Definition A.2.1.** Let $C, D$ be relative Seely categories. A relative Seely functor $C \to D$ is a functor $F : C \to D$ which restricts to $F : C_s \to D_s$, equipped with:

* For every $A, B \in C$, natural isomorphisms morphisms

$$ 
\begin{aligned}
t_{A,B}^{\otimes} & : FA \otimes FB \cong F(A \otimes B) \\
t^1 & : 1 \cong F1;
\end{aligned}
$$

making $(F, t^{\otimes}, t^1)$ a strong symmetric monoidal functor $(C, \otimes, 1) \to (D, \otimes, 1)$;

* for every $S, T \in C_s$, isomorphisms

$$ 
\begin{aligned}
t_{S,T}^{\&} & : FS \& FT \cong F(S \& T) \\
t^{\top} & : \top \cong FT;
\end{aligned}
$$

* For every $A \in C$ and $S \in C_s$, an isomorphism

$$ t_{A,S}^{\to} : FA \to FS \cong F(A \to S); $$

* For every $S \in C_s$, an isomorphism

$$ t_S^1 : !FS \cong F!S; $$
satisfying the coherence axioms of Figure A.1, and the naturality-like condition that for every $S, T \in C_S$ and $\sigma : !S \to T$, the following diagram commutes:

<figure><img src="image_253.png" /></figure>

**Lifting to the Kleisli categories.** Given a relative Seely functor $F : C \to D$, we define its **lifting** to a functor $F_! : C_! \to D_!$ that we shall prove to be cartesian closed.

On objects, we simply set $F_!(S) = FS$. On morphisms, for $\sigma : !S \to T$, we set

$$F_! \sigma = F \sigma \circ t_S^! : !FS \to FT.$$

From this data, a routine calculation ensures that we have:

**Proposition A.2.2.** *The above data yields a functor $F_! : C_! \to D_!$.*

Next, we show that this functor is cartesian. By definition, this means that $FT$ is terminal – which is clear from $t^T$ – and that for all $S, T \in C_!$, the canonical map

$$\langle F_! \pi_S^! , F_! \pi_T^! \rangle_! \in D_!(F(S \& T), FS \& FT)$$

obtained via the cartesian structures of $C_!$ and $D_!$, is invertible. Now using our coherence laws, this morphism simplifies to $\langle F\pi_S \circled_{S,T}, F\pi_T \circled_{S,T} \rangle : !F(S \& T) \to FS \& FT$. And indeed, the inverse we seek can be constructed as

$$r_{S,T}^{\&} = t_{S,T}^{\&} \circ \mathrm{der}_{FS \& FT} : ! (FS \& FT) \to F(S \& T);$$

that it is an inverse is a direct verification via our coherence laws, which ensure that $t_{S,T}^{\&}$ is an inverse in $D$ to the canonical map $\langle F(\pi_S), F(\pi_T) \rangle : F(S \& T) \to FS \& FT$ given by the cartesian closed structures in $C$ and $D$.

Likewise, proving that $F_!$ is cartesian closed means showing, for all $S, T \in C_!$, that

$$\Lambda^!(F_!(ev_{S,T} \rightharpoonup) \circ r_{S,T} \rightharpoonup) \in C_!(F(S \Rightarrow T), FS \Rightarrow FT)$$

obtained via the cartesian closed structures of $C_!$ and $D_!$, has an inverse. But via our coherence rules, this morphism simplifies to the composition in $D$:

$$!F(!S \to T) \xrightarrow{\mathrm{der}_{F(S \to T)}} F(!S \to T) \xrightarrow{(t_{S,T}^{\to})^{-1}} F(!S) \to FT \xrightarrow{t_S^{\to} \to FT} !FS \to FT,$$

where we use that as usual, relative closure informs a contravariant functor $- \to S : D^{\mathrm{op}} \to D$ for all $S \in D_S$, defined as $\sigma \to S = \Lambda(ev_{B,S} \circ ((B \to S) \otimes \sigma)$ for any $\sigma : A \to B \in D$. Now, the morphism above has an inverse in $D_!$, constructed as

$$r_{S,T} = t_{S,T}^{\to} \circ ((t_S^{\to})^{-1} \to FT) \circ \mathrm{der}_{FS \to FT} : !(!FS \to FT) \to F(!S \to T)$$

concluding the proof of the following statement:
<figure><img src="image_254.png" /><figcaption>Figure A.1: Coherence diagrams for relative Seely functors</figcaption></figure>
**Theorem A.2.3.** Consider $F : C \to D$ a relative Seely functor.

Then, the functor $F_1 : C_1 \to D_1$ constructed above is cartesian closed.

All the axioms of relative Seely functors get used in the proof, except for the last coherence diagram of Figure A.1, which appears unnecessary to ensure that a relative Seely functor lifts to a cartesian closed functor between the Kleisli categories. We include it nonetheless, as it seems likely to be necessary if we ever wish to show that relative Seely functors preserve the interpretation of a linear/non-linear type system.