Simon Castellan

Game Semantics: Easy as Pi Introducing Programming Game Semantics

Keywords: game semantics, -calculus, session types, Linear Logic, event structures

Game semantics has proven to be a robust method to give compositional semantics for a variety of higherorder programming languages. However, due to the complexity of most game models, game semantics has remained unapproachable for non-experts.

In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation into a session typed -calculus, referred to as metalanguage, followed by a semantics interpretation of the metalanguage into a particular game model. The syntactic translation can be defined for a wide range of programming languages without knowledge of the particular game model used. Simple reasoning on the model (soundness, and adequacy) can be done at the level of the metalanguage, escaping tedious technical proofs usually found in game semantics. We call this methodology programming game semantics.

We design a metalanguage ( DiLL ) inspired from Differential Linear Logic (DiLL), which is concise but expressive enough to support features required by concurrent game semantics. We then demonstrate our methodology by yielding the first causal, non-angelic and interactive game model of ML , a higher-order call-by-value language with shared memory concurrency. We translate ML into DiLL and show that the translation is adequate. We give a causal and non-angelic game semantics model using event structures, which supports a simple semantics interpretation of DiLL . Combining both of these results, we obtain the first interactive model of a concurrent language of this expressivity which is adequate with respect to the standard weak bisimulation, and fully abstract for the contextual equivalence on second-order terms.

We have implemented a prototype which can explore the generated causal object from a subset of OCaml.

INTRODUCTION

Background. Reasoning about programs requires a mathematical model of their execution, called semantics. A popular technique is operational semantics which models the concrete execution on the metal by an abstract machine made of mathematical symbols and Greek letters. Its popularity is due to its simplicity and flexibility, modelling a wide range of programming features. However, operational semantics only gives meaning to closed programs of ground types. Open higher-order programs, ie. programs with external functional parameters are left aside. This creates difficulties, for instance, comparing such programs can only be done through an untractable quantification over arbitrary contexts. Denotational semantics tackles this problem by trying to give compositional semantics, usually as a function from its external parameters to the result. The most common form of denotational semantics, based on domain theory, copes well with higher-order functions, but more laboriously with effectful computations, and almost not at all with concurrency.

At the dawn of the 1990s, a new form of denotational semantics appeared: game semantics [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On full abstraction for PCF[END_REF]. There, an open program is modelled by its possible interactions with the context. Thanks to its interactivity, this methodology has proved to be very extensible and easily supports a wide range of programming features (references, control operators, probabilities, concurrency, quantum, etc.) Moreover, as observed by [START_REF] Ghica | A System-Level Game Semantics[END_REF], game semantics reconciles denotational and operational semantics together: the interaction traces of a program can be computed either denotationally (by induction on the syntax) or operationally (by running an abstract machine).

While game semantics has been recognised as a powerful tool to build denotational models, we believe that its most useful and promising feature is the simplicity with which one can describe the compositional behaviour of systems in general (eg. with its recent use for verifying compilers [START_REF] Koenig | Refinement-Based Game Semantics for Certified Abstraction Layers[END_REF][START_REF] Stewart | Compositional CompCert[END_REF] or operating systems [START_REF] Gu | Certified Concurrent Abstraction Layers[END_REF]). So far, its simplicity has not been apparent, and game semantics is often considered inaccessible to nonexperts who wish to define a denotational model based on games for their favourite language.

The Framework. The thesis of this paper is that, the complexity of game semantics interpretations can be decomposed by introducing a simple message-passing intermediate language, between the source program and the model. Indeed, game semantics bundles two ideas together: the idea of interpreting a program as a process interacting with its environment, and a semantic interpretation of these processes. Our main contribution in this paper is to make this separation explicit by factorising the interpretation of a language in game semantics as the following steps: This factorisation offers several advantages. First, it allows to decouple the interpretation of the source language from the details of the model. One can use the same translation to obtain different models (eg. traces, event structures, LTSs, ...), and, conversely, one can interpret a language becomes a matter of writing a syntactic translation, an easier task than doing the interpretation from a language to a game model directly, and which becomes model-agnostic.

A Language for Strategies. What would a good intermediate language for strategies be? Strategies represent the interaction of the program with the environment in the form of messages that are exchanged between them. For that reason, a message-passing language such as the -calculus [Milner et al. 1992] is an ideal candidate. Dating back to encodings of the call-by-name and call-by-value -calculi by Milner [1992a], the -calculus has been used to encode a wide range of programming languages, including functional, concurrent, and distributed languages. Its connection with game semantics has been studied ever since the introduction of game semantics [START_REF] Hyland | Pi-Calculus, Dialogue Games and PCF[END_REF]. Some game semantics interpretations rely on the use of the categorical semantics of Linear Logic [START_REF] Melliès | Categorical semantics of linear logic[END_REF]]. Recently, [START_REF] Caires | Session Types as Intuitionistic Linear Propositions[END_REF] have discovered a Curry-Howard correspondence between the -calculus and Linear Logic through session types. Specifically, this paper uses an extension of the calculus in [START_REF] Wadler | Propositions as sessions[END_REF]] to Differential Linear Logic (DiLL) [START_REF] Ehrhard | An introduction to differential linear logic: proof-nets, models and antiderivatives[END_REF] where ⊗ and `are identified to be able to interpret languages with deadlocks. Session types are a natural fit here since their connection with game semantics have been recently discovered [START_REF] Castellan | Two Sides of the Same Coin: Session Types and Game Semantics[END_REF] (in a prototypical setting). Our metalanguage is going beyond other session type-based calculi to be able to express game semantics interpretations.

Contributions and Outline of the Paper. This paper proposes a uniform framework where we view game semantics interpretations as syntactic translations to a process calculus, followed by a semantic interpretation of this calculus into a game model.

We demonstrate this methodology using one translation and one semantics interpretation: we translate ML , which is a mini ML extended with shared memory concurrency into the metalanguage, DiLL based on Differential Linear Logic. 1 Our semantic interpretation of DiLL is based on an extension of concurrent games [START_REF] Rideau | Concurrent Strategies[END_REF], that deals with internal actions and replication. Combining the syntactic translation and semantics interpretation gives us the first causal and interactive interpretation of a concurrent call-by-value language, which is adequateand fully-abstract for second-order interfaces -for a strong notion of contextual equivalence. This bridges the gap with real-world programming languages, as our implementation of the model allows to explore the causal behaviour of concurrent programs written in (a subset of) OCaml.

: int → int ⊢ 1 + 2 : int
The methodology is illustrated in Figure 1 on a program calling an external function twice in parallel, as function parameters are executed in parallel in this language. This program is translated to the -calculus which is then interpreted as an event structure describing the causal relationships between the different actions of the program (see § 4 and § 5).

Our paper is structured as follows: § 2 presents an overview of the paper and introduces the source language ML ; § 3 presents our metalanguage DiLL and its equational theory; § 4 presents the translation of ML into DiLL ; § 5 presents the causal model of the metalanguage; § 6 presents the interpretation of DiLL into the model; § 7 outlines our prototype implementation of a causal interpretation of a subset of OCaml. § 8 provides related work and § 9 concludes with future work. work. Proofs can be found in Appendix, and we shall submit our prototype implementation to Artifact Evaluation.

We make use of the knowledge package. Definitions of mathematical concepts appear blue boldface, and their uses occur in blue and are linked to the original definition.

OVERVIEW: GAME SEMANTICS AS MESSAGE-PASSING TRANSLATION

In this section, we informally introduce our methodology. In particular, we explain basic ideas behind game semantics interpretations, and their syntactic counterpart in our metalanguage. This section paves the way to the formal definition of DiLL in § 3. In § 2.1, we first introduce our source language, a concurrent call-by-value language, ML . We then illustrate different aspects of the language and the techniques we use to represent them: § 2.2 focuses on first-order terms; § 2.3 on higher-order behaviour; and finally § 2.4 discusses shared memory.

ML : Mini-ML with shared-memory concurrency

We use a concurrent call-by-value language with integer references, called ML :

type , ::= • | int | bool | ref | → value ::= | . | | tt | ff | () term , ::= | | | ⊥ | if ′ | plus | equal | get | set | ref
A base type is either the unit type written •, int or bool. is the fixpoint operator. We use standard syntactic sugar: let = in for ( . ) ; let = in for let = . in . Note that our language does not include products or sum types for presentation purposes. It is straightforward to extend our approach to those, and our implementation supports them.

Δ, : ⊢ : [ ] Δ, : ⊢ : Δ ⊢ . : → [ ] Δ ⊢ : → Δ ⊢ : Δ ⊢ : [ ] Δ ⊢ ⊥ : [ ] Δ ⊢ : (( → ) → ( → )) → → [ ] Δ ⊢ tt, ff : bool [ ] Δ ⊢ : bool Δ ⊢ 1 : Δ ⊢ 2 : Δ ⊢ if 1 2 : [ ] Δ ⊢ : int [ ] Δ ⊢ plus : int → int → int [ ] Δ ⊢ () : • [ ] Δ ⊢ ref : int → ref [ ] Δ ⊢ get : ref → int [ ] Δ ⊢ set : ref → int → • [ ] Fig. 2. Typing system of ML
Instead of having specific constructs (eg. := ), we chose to have higher-order constants which makes the metatheory simpler. Hence, we write + for plus ; = for equal ; ! for get ; := for set . We have not included any sequential or parallel composition operators in the language as it is definable in the language: ; is a shorthand for ( . ) when not occurring free in and is a shorthand for ( . ()) : this behaves as expected due to our semantics of application, which evaluates arguments in parallel.

Typing of this language is standard, given by a judgement Δ ⊢ : where Δ = 1 : 1 , . . . , : and is shown in Figure 2. The terms equal, plus, get, set, and ref are called constants. An interface is a pair of a context Δ and a type , written Δ ⊢ .

Operational Semantics. As it is customary for such languages mixing higher-order and shared state, we define the operational semantics in two steps: we first define a confluent reduction relation → on all terms, which only reduces functional redexes, leaving reference operations unchanged. The rules for this reduction relation are standard and given in Figure 3a, where we use the following evaluation contexts: :

:= [ ] | | | if
. This choice of contexts implies in particular that in the evaluation of and are done in parallel: This allows for operators that evaluate their arguments in parallel; e.g. + , which unfolds to plus , evaluates and in parallel. Sequentiality is only ensured between the body of a function and its argument: in ( . ) , is always evaluated first. Since is simply defined as ( .()) , this also guarantees that and are evaluated in parallel.

In a second step, we look at terms of the form Δ ⊢ : where (1) is not a functional type; and Δ( ) = ref for all ∈ dom(Δ). Such terms are called semiclosed, and are going to be executed by a machine whose states are tuples Δ ⊢ ì

, where Δ ⊢ : is semiclosed, ì is a subset of dom(Δ), the public locations; and : dom(Δ) → N is the memory state, mapping locations to values. The type is the type of the machine Δ ⊢ ì , .

We chose to give the operational semantics of such machine states under the form of a labelled transition system. The visible actions will correspond to memory actions described by Σ ML ::= r , | w , where is a free reference variable and ∈ N is a value: r , means the program has read value from , and w , that it has written to . The transitions of the LTS are labelled over the set Σ ML ∪ { }, which is ranged over by , . The silent action is often omitted. The LTS of ML is given in Figure 3b. Note that ì stays unchanged through out the reduction.

L 2.1 (S R ). (1) If Δ ⊢ : and → , then Δ ⊢ : ; and (2) if Δ ⊢ : is semiclosed and Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ then Δ ′ ⊢ : .
Weak bisimulation and observation equivalence. We define the standard weak bisimulation relation between two machines as equivalence on base terms. By the LTS rules in Figure 3, weak transitions are defined as expected: we write =⇒ for the reflexive, transitive closure of -→, =⇒ for transitions =⇒ -→=⇒, and

ˆ =⇒ for =⇒ if ≠ and =⇒ otherwise. a value ( . ) → [ / ] [ ] + → + [ ] = → tt [ ] ≠ = → ff [ ] if tt → [ ] if ff → [ ] , ′ are values ′ → ( ) ′ [Y] → [ ] → [ ] [ ] (a) Deterministic reduction for functional fragment of ML → Δ ⊢ ì , -→ Δ ⊢ ì , [ ] ∈ dom(Δ) ∈ ì ⇒ = w , ∉ ì ⇒ = Δ ⊢ ì := , -→ Δ ⊢ ì (), [ := ] [ ] Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ Δ ⊢ ì [ ], -→ Δ ′ ⊢ ì ′ [ ], ′ [ ] ∈ dom(Δ) ∈ ì ⇒ = r , ( ) ∉ ì ⇒ = Δ ⊢ ì ! , -→ Δ ⊢ ì ( ), [ ] ∉ dom(Δ) Δ ⊢ ì ref( ), -→ Δ, : ref ⊢ ì , [ := ] [ ] (b) Labelled Transition System for ML semiclosed terms Fig. 3. Operational semantics of ML Definition 2.2 (Weak bisimulation of ML machines). A relation R over machines of type • is a weak bisimulation if (1) for all Δ 1 ⊢ ì 1 , 1 R Δ 2 ⊢ ì 2 , 2 , whenever Δ 1 ⊢ ì 1 , 1 -→ Δ ′ 1 ⊢ ì ′ 1 , ′ 1 , there exists Δ 2 ⊢ ì 2 , 2 ˆ =⇒ Δ ′ 2 ⊢ ì ′ 2 , ′ 2 such that Δ ′ 1 ⊢ ì ′ 1 , ′ 1 R Δ ′ 2 ⊢ ì ′ 2 , ′ 2 .
(2) The symmetric case of 1. The largest such bisimulation is called weak bisimilarity, denoted by ≈ ML .

We define the observational equivalence on terms by quantifying over machine contexts.

Definition 2.3 (Observational equivalence of ML ). Given Δ ⊢ , : , and are observationally equivalent, written ≅ ML when for all machine contexts of • type (that is a machine of • type with a hole in the term component), [ ] ≈ ML [ ].

First-order programs

We start our investigation of the interactive semantics of ML with the first-order case. An interface Δ ⊢ is first-order when is a base type and Δ only contains base types. In call-by-value, such terms have a limited interaction with their environment, as variables stand for values: waiting for the values of its parameters from the environment, computing the result, and finally possibly returning it to the environment (or diverging).

For each type , we define a set ℭ( ) of messages describing values of type . For base types, ℭ( ) is exactly the set of values of :

ℭ(int) = N ℭ(•) = {()} ℭ(bool) = {tt, ff}.
For non-base types, as we will see in the next section, this correspondence will not hold. This extends to context by letting ℭ(Δ) be the set of tuples ∈dom(Δ) ℭ(Δ( )). So, the protocol of a first-order interface Δ ⊢ is very simple: Program expects a tuple of constructors for its parameters (an element of ℭ(Δ)) and then may return its result, a constructor of .

Unsurprisingly, our language of session types must then include type constructors representing of messages will be seen as inputs (and be assigned a negative polarity) while the second kind will be seen as outputs (and assigned a positive polarity).

We use here a dialect of session types inspired by Linear Logic, and this data flow is captured by the additive connectives: & (input) and ⊕ (output). Concretely, the translation of a first-order interface Δ ⊢ gives the following protocol:

Δ ⊢ = & ∈ℭ(Δ) Call( ) -•⊕ ∈ℭ ( ) Ret( ) + :
Program must input a message Call( ) containing the parameter values and may output a message Ret( ) with its return value.

The interpretation of a first-order type is simply the process that waits for the input parameter, computes the value and returns it. This process is parametrised by a name representing the communication channel with Context. For instance, the negation is:

: bool ⊢ neg def = if ff tt : bool = & {Call(tt) ( ). ⊕ Ret(ff); Call(ff) ( ). ⊕ Ret(tt)}.
It starts by an input on and there are two branches since we can receive two possible values. Along with the value received, there is also a new name ( ) which is used for the continuation of the protocol: in this case, returning the result. (We will see soon that in this particular case it is possible to reuse the name , as is customary in session types, but in general it is not possible.)

In the semantic world, the session type Δ ⊢ becomes a game (where moves are messages), and the process Δ ⊢ : becomes a strategy, which in our setting explicits the causal relationships between the different actions of the program (in ML : memory operations, calls and returns). Both games and strategies are described by the same mathematical object: an event structure, which is a partial order (written ) along with a conflict relation ( / o ). In the example of the negation, we have drawn both the game and the strategy in Figure 4. Conflict represents incompatibility within an execution: two events in conflict will occur in different executions. In games, this represents the fact that the protocol forbids to play these two moves in the same execution, corresponding to choices (& and ⊕) in the syntax of session types: Context has to choose a set of parameters, and Player a return value. Note that in this simple case, the strategy is simply a subset of the game.

Higher-order programs

This might seem a lot of complexity to capture simple input/output behaviours. However, it becomes justified when looking at higher-order programs where the control jumps between Program and Context due to calling external functions, i.e.. functions of the interface. Let us start with a simple (second-order) example : • → • ⊢ := (); () : •. As before, Context starts by sending a constructor for each parameter. But what should be a constructor for the type • → •? In game semantics, we explicitly observe function calls and returns across the interface. To model this, Context sends a token, which we write simply , instead of sending a function or some code. However, now the session between Program and Context is split in two independent sub-sessions: one, as before, for Program to return the result, and a second one to make calls to . To represent this splitting of a session into several sub-sessions, we use the notation , which represents the

0 Req + 1 Ret() + Call() + Call() + . . . Ret() - Ret() - . . . : • → • ⊢ • Call( ) - Call( ) - Req + 0 Req + 1 Ret() + Call() + Call() +
Ret() - Ret() - Fig. 5. Interpretation of higher-order terms multiplicative connectives of Linear Logic (⊗, `) identified into one. 2 The interface thus becomes:

: • → • ⊢ • = Call( ) -• (Call() + • Ret() -Ret() + ).
where we use Call( ) -• instead of the unary choice & ∈{ * } Call( ) -• and similarly for Call() + • . In this protocol, Program receives the token from Context, and then can either call or return. If Program calls , then it might return (). However, there is some information that is not captured here. Program should be allowed to call several times, but may only return only once: certain sessions can be repeated while some others may not. To encode this information in the session type, we use the standard exponentials of Linear Logic: by default every message is linear (can only occur once). Then, we have two dual modalities that allow to specify duplication: ? means Program can spawn as many instances of as they like; while ! means Context can spawn as many instances of as they like, hence Program must behave as a server accepting requests from Context.

Our example requires ?(•) since Program decides how many times is called. We get:

: • → • ⊢ • = Call( ) -• (?(Call() + • Ret() -) Ret() + ). = & Call( ) ( , ). ? [ ]. ⊕ Call() [ 1 ]. 1 & Ret(). ? [ ]. ⊕ Call() [ 2 ]. 2 & Ret(). ⊕ Ret()
The above example features two new constructs. First, due to , it is possible to introduce several names (in the input on ), as there might be several sub-sessions now: for instance, denotes here the session related to while that related to returning the result. Second, we have the construction ? [ ] which opens a new session (of type ) on called when has type ? . In this case, sessions on name are used to make a call to parameter . Note that we can reuse the name across sessions as, being a linear name, it disappears after the ⊕ Call(). The interpretation of and its interface are given in Figure 5. The game is now more complex: we see clearly the possible independent sub-sessions as being incomparable for the causal order. The ? construction is putting infinitely many copies of , each prefixed by a positive move Req equipped with a copy index ∈ N. When the strategy plays, it chooses indices for the positive moves: this choice is irrelevant (two different choices will yield equivalent strategies). In this case, the strategy is still a subset of the game, but there are now extra causal links indicating the sequentiality specific to the term (arrows in red).

By duality, the ! construction is used when defining functions. To construct a process implementing a session type ! , we use a construct called promotion, written ! ( ). , which represents a server spawning up each time a request is made, with being the request. For instance, we have:

⊢ • → • = Call() -• ( + • !(Call() -• Ret() + )) .() = & Call(). ⊕ . ! ( ). & Call(). ⊕ Ret().
A function starts by telling Context that it does normalise to a -abstraction, by sending , and then sets up a server to handle calls to the function by Context. In this term, we have not specified a list of names for some actions: this means we simply reuse the subject of the action, for instance ⊕ stands for ⊕ [ ].

Shared memory concurrency

To conclude our illustration of the phenomena at play in the game semantics of a language like ML , we now outline the case of references. However, such a server cannot be implemented using the promotion described in § 2.3. Indeed, such servers are stateless, meaning that the answer to a request does not depend on previous or parallel requests. In particular, two independent requests can (and are) treated independently. This is not the case for a server implementing a reference, which has to treat requests in a sequential order. Two independent request must thus be sequentialised. To represent this phenomenon, we turn our attention to an extension of Linear Logic, called Differential Linear Logic [START_REF] Ehrhard | An introduction to differential linear logic: proof-nets, models and antiderivatives[END_REF]], which extends Linear Logic with such servers. We use here a slight variant of the standard codereliction, which allows to set up a one-time server. Such "servers", written # ( ). in our metalanguage introduced in the next section, wait for one request , and execute on it. has still access to so it can start a new such server if it wants to, after having processed the request . In the meanwhile, the server is down, and requests are left pending. In particular two concurrent requests are racing to be satisfied by this server. This phenomenon induces a natural sequentialisation of the requests on . The implementation of this reference server is given in § 4.2.

3

DiLL : A METALANGUAGE FOR STRATEGIES OF GAME SEMANTICS In this section, we present a formal treatment of the intuitions presented in § 2, and formalise it into a calculus that we call DiLL , as its typing rules are close to Differential Linear Logic (DiLL). In § 3.1 we present the types of DiLL ; in § 3.2 we present the syntax of the calculus for session types and processes along with the typing discipline. In § 3.3 we define the operational semantics of DiLL ; and in § 4 we present the interpretation of ML into DiLL .

Types of DiLL

As explained in § 2, our types closely mirror the syntax of Linear Logic formulas:

& ∈ ℓ -• | ⊕ ∈ ℓ + • | ( . . . ) | ? | ! .
These types describe protocols from the point of view of Program. The first two are the additive connectives and represent data input and data output respectively: & ∈ ℓ -• means that Program should expect a message consisting in one of the ℓ from Context and then behave as the corresponding ; and dually ⊕ ∈ ℓ + • indicates that Program should output to Context one of the ℓ and continue as the corresponding . In both instances, is an arbitrary countable set of choices; and ℓ represents the payload of the message, to be thought of simple datatypes such as integers or booleans choosen in a set L. When is a singleton we write ℓ -• and ℓ + • directly.

The construct 1 . . . is the parallel composition and represents both `and ⊗: in this setting with deadlocks, we do not need to distinguish between the two multiplicatives connectives of Linear Logic and can identify them (as in compact-closed models of Linear Logic). From a protocol standpoint, this means that the current session splits into independent subsessions. In Session Types, these two connectives are called input and output respectively and represents delegation, or channel-passing. However, in this setting closer to the internal -calculus [START_REF] Sangiorgi | pi-Calculus, Internal Mobility, and Agent-Passing Calculi[END_REF]] where free names are never sent, the right intuition is that channels are not passed around, but messages occurring in one of the subsession is just prefixed with the index of the sub-session (thus encoding the so-called multiplicative addresses), and the names are just abstraction around these addresses. A parallel composition can be empty, leading to the type 1, which is the equivalent of the (identified) multiplicative identities of Linear Logic.

The dual types ! and ? are the exponentials and represent replicable sessions: ! means that Program is expected to receive arbitrarily many queries from Context to start a session of type (ie. Program is the server, and Context the client); while ? means that Program can contact Context to start as many sessions of type as it wants (ie. Program is a client and Context the is a server).

Types come equipped with a notion of duality stemming from the usual De Morgan laws: & and ⊕ are dual to each other, as well as ? and ! while and 1 are self-dual. Session types whose toplevel constructors are not are called rooted as they have a unique minimal action. Only such types will be bound to channels in DiLL .

Processes of DiLL

The syntax of DiLL follows the notation of [START_REF] Wadler | Propositions as sessions[END_REF].

, ::= 0 | | ( ) | & {ℓ ( ì ). } ∈ | ⊕ [ ì ]. | ! ( ì ). | # ( ì ). | ? [ ì ].
0 denotes a nil process, is a parallel composition, ( ) is a restriction where binding and in . & { ( ì ). } ∈ is a branching with labels ℓ ∈ L indexed by ∈ where can be infinite; its dual, ⊕ [ ì ]. , is a selection to label . promotion ! ( ì ). (stateless server), codereliction # ( ì ). (stateful server), and dereliction ? [ ì ]. (their client) have been explained in § 2. In all constructs, ì , ì are lists of bound names as in the internal -calculus [START_REF] Sangiorgi | pi-Calculus, Internal Mobility, and Agent-Passing Calculi[END_REF]].

We consider the finite or infinite processes generated by this grammar. Concretely, we consider the set of processes to be the ideal completion of the finite processes ordered by the subtree ordering. This is standard in some literature of the -calculus (eg. [START_REF] Castagna | Contracts for Mobile Processes[END_REF]) and necessary to give a syntactic counterpart to infinite strategies which are used in the interpretation of most languages, for recursion and memory. Definition of such infinite processes will mostly be by computing the least fixpoint of continuous functions. Such fixpoints are written fix .

Typing rules. We now describe the typing rules for the calculus. Typing contexts are of the form Γ := 1 : 1 , . . . , :

where each is a rooted type. This is key since we want every action of our -calculus to correspond to a meaningful computational event.

While typing judgements are flat lists, session types have more structure since ( ) is only equivalent to ( ) (ie. isomorphic as games as will be seen in § 6.1), but not equal. This prompts us to define a way to flatten a non-rooted session type into a context. For that, we define (when is rooted) ì , ì :: ( ) ≔ ì :: , ì :: . and undefined otherwise. Note that for the second equation, the decomposition in ì , ì of any list ì is unique, given type of where ì and ì are assigned by and , respectively. We write • for the empty list of names. Note that • :: 1. Typing judgements are simply of the form ⊲ Γ. The rules are described in Figure 6. (As for the syntax of untyped terms, we consider the infinite derivation tree generated by these rules.)

[ ] [ ] [ ] [ ] [ ] 0 ⊲ Γ ⊲ ?Γ, Γ 1 ⊲ ?Γ, Γ 2 ⊲ ?Γ, Γ 1 , Γ 2 ⊲ Γ, : , : ⊥ ( ) ⊲ Γ ⊲ ?Γ, ì :: ! ( ì ). ⊲ ?Γ, : ! ⊲ Γ, : ? , ì :: ? [ ì ]. ⊲ Γ, : ? [ ] [ ] [ ] ∀ ∈ , ⊲ Γ, ì :: & {ℓ ( ì ). } ∈ ⊲ Γ, : & ∈ ℓ -• ∈ ⊲ Γ, ì :: ⊕ ℓ [ ì ]. ⊲ Γ, : ⊕ ∈ ℓ + • ⊲ Γ, : ! , ì :: # ( ì ). ⊲ Γ, : !
The rule [ ] allows us to weaken any name preserving typability; note that DiLL is affine and not linear: this mirrors a similar phenomenon in game semantics. The rule [ ] forces the split of the linear part of the context in a parallel composition. The rule [ ] introduces two connected channels with dual types.

The rule [ ] is the introduction rule for !, and corresponds to setting up a server on which spins up a new copy of whenever a request is made. As usual in Linear Logic, since might be duplicated, the session types in Γ must be of the form ? , which we indicate with the notation ?Γ. The dual rule [ ] sends a request to a server. Note that is still usable in the continuation.

The rule [ ] is selection, an output of a payload to the other party on a channel. In the continuation, the name disappears as it has been consumed, and the new names ì appear: they are used to deconstruct the continuation type . We have a non-trivial list as soon as is not rooted. The dual rule [ ] represents branching: every possible message that can be received must be handled.

The rule [ ] arises from Differential Linear Logic and corresponds to setting up a server that accepts exactly one request, and then disappears. Unlike rule [ ], the continuation might use again, and set up a new server later on. Two concurrent requests made on these one-time servers will race to be accepted, creating nondeterminism. This rule merges codereliction and cocontraction of DiLL in one single rule. We found easier to give non-angelic semantics to this presentation as semantics of DiLL is usually angelic. However, the usual codereliction and cocontraction are admissible from this rule.

When writing down processes, we often omit the list of successors ì . This may mean two things: if the move is maximal, it has no successors and we omit the empty list ; if the move has a unique successor, we use the standard convention of session types which reuses the same session name, eg. we write ⊕ for ⊕ [ ]. This is only valid if does not have type ? since it can then be reused. In general we also reuse linear names along a session.

The forwarding agent. We introduce the forwarding agent [ ì ↔ ì ] ⊲ ì :: , ì :: ⊥ for any session type and ì :: and ì :: ⊥ defined. The forwarding agent represents copycat in game semantics. It is defined by induction on , by following the -expansion laws in Linear Logic:

[ ↔ ] & ∈ ℓ • = & {ℓ ( ì ). ⊕ ℓ [ ì ]. [ ì ↔ì ] } ∈ [ ↔ ] ! = ! ( ì ). ? [ ì ]. [ ì ↔ì ] [ ì ↔ ì ] 1 ... = 1≤ ≤ [ ì ↔ ì ] [ ↔ ] ⊥ = [ ↔ ]
Composition of processes. A key operation in game semantics is composition. It allows defining the interpretation of a programming language by introducing small bricks that can be composed together. This composition can be expressed in this setting as is well-known:

ì ⊙ := ( ì ì ¯ ) ( ) ⊲ Γ 1 , Γ 2 , ?
Γ where ⊲ Γ 1 , ?Γ, ì : ì and ⊲ Γ 2 , ?Γ, ì ¯ : ì ⊥ This mimimcks the traditional definition using parallel interaction with hiding. We use here the notation but not with its standard -calculus meaning: here and are simply two independent names which only become related via the restriction.

Operational semantics of the metalanguage

We define the operational semantics of DiLL . As for ML , it will be done in two steps: (1) a congruence that will contain the usual structural congruence of the -calculus, the permutation rules due to courtesy in game semantics, and finally the deterministic communication, and (2) an operational semantics which resolves the races induced by the codereliction/dereliction pairs.

Congruence. We start with the congruence on our calculus, which takes into account the asynchronous permutations, needed for the game semantics. These permutations are necessary to obtain a category, which is essential to interpret functional languages. These asynchronous permutations include all permutations between actions on distinct channels of the same polarity, among others. To formalise them, we use the notion of prefix. A prefix is a pair of an arity and a context with as many holes as the arity, as defined by:

::= ⊕ [ ì ]. [] | ? [ ì ]. [] | & {ℓ ( ì ). [] } ∈ | ! ( ì ). [] | # ( ì ). []
The arity of all prefixes is one, except the branching prefix whose arity is the indexing set . Given a prefix with arity , and a family of process ( ) ∈ , we write [ ] ∈ for the substitution. A prefix is positive (written + ) when it is a selection or dereliction; and negative otherwise (written -).

We also adopt the convention that a prefix is a prefix of polarity on channel . We write bv( ) for the set of bound variables occurring in the pattern in . Two prefixes and are orthogonal, written ⊥ when ({ } ∪ bv( )) ∩ ({ } ∪ bv( )) = ∅. The structural congruence on finite processes is defined as the smallest congruence on well-typed terms (over the same context) satisfying the rules described in Figure 7. The first box defines the standard structural congruence rules. The second box explains how prefixes commute with each other and other construct. The premise of [ ] ensures the typability of both sides of processes. The last rule [ ] is very important and states that the asynchronous forwarder behaves as an identity. This induces most asynchronous permutations. The fourth box is about deterministic communication. We consider them as a part of the congruence rules as we perform them under context -since they are deterministic, it does not matter when or where they are performed.

These rules are extended to infinite processes in the obvious continuous way: ≡ when for all finite 0 ≤ , then there exists 0 ≤ with 0 ≡ 0 and vice-versa.

Example 3.1. Remember the process of Figure 1 representing two parallel calls to the same external function. This term is equivalent to the following:

≡ &Call( ) ( , ). ? [ ]. ⊕Call(1). ? [ ′ ]. ′ ⊕Call(2). &Ret( ). ′ &Ret( ). ⊕Ret( + ).
This illustrates that, due to those permutations, processes that seem sequential (ie. without ) can actually be concurrent due to these asynchronous permutations: only syntactic dependence from input to output is preserved.

and restriction 0 ≡ ≡ ( ) ≡ ( ) ( )0 ≡ 0 ( ) ≡ ( ) { , } ∩ { , } = ∅ ( )( ) ≡ ( )( ) fv( ) ∩ { , } = ∅ ( )( ) ≡ (( ) )
Permutations of prefixes Reduction rules of DiLL . We define the operational semantics of DiLL , which now only reduces redexes involving a dereliction and a codereliction. This redex is nondeterministic because the reduction consumes the codereliction: hence two concurrent derelictions race for the codereliction. The rules of the LTS for finite processes are defined in Figure 7, where ::

( ) -[ ] ∈ ≡ 0 [ ] ∉ { , } ( ) [ ] ∈ ≡ [( ) ] ∈ [ ] ∉ { , } ( )( -[ ] ∈ -[ ] ∈ ) ≡ -[( )( -[ ] ∈ )] ∈ [ ] ⊲ Γ, : ⊙ [ ¯ ↔ ] ≡ [ / ] [ ] Deterministic communication ∈ ( )( ⊕ [ ì ]. & { ( ì ). } ∈ ) ≡ ( ì ì )( ) [ ] ( )(? [ ì ]. ! ( ì ). ) ≡ ( )(! ( ì ). ( ì ì )( )) [ ] ( )( ! ( ì ). ) ≡ ( )( ! ( ì ). ) ( )( ! ( ì ). ) [ ] Reduction rules ( )(? [ ì ]. # ( ì ). ) → ( )( ( ì ì )( )) [ ] → [ ] → [ ] [ ] ′ ≡ → ≡ ′ → [ ]
= [] | | (
) . As before, we extend the LTS to infinite processes by letting → when is the limit of all 0 ≤ such that there exists 0 ≤ with 0 → 0 . For the proof of Lemma 3.2, see Appendix A.1.

L 3.2 (S R ). If ⊲ Γ and → , then ⊲ Γ.
Observational theory. From this operational semantics, we deduce a notion of behaviour equivalence through the standard concept of reduction-closed barbed congruence [START_REF] Honda | On Reduction-Based Process Semantics[END_REF][START_REF] Milner | Barbed Bisimulation[END_REF]. First, let us define the notion of barbs: a process has a barb on , written ⇓ if ≡ ( ì ì ) ( + [ ] ).

Definition 3.3. A reduction-closed barbed congruence is an equivalence relation on typed processes R containing ≡ such that:

• If ( , ) ∈ R, then ⇓ iff ⇓ • If ( , ) ∈ R and → ′ then there exists ( ′ , ′ ) ∈ R such that → * ′ . • If ( , ) ∈ R then for all context , ( [ ], [ ]) ∈ R.
We write ≅ DiLL for the largest reduction-closed barbed congurence. This section defines the translation of ML into DiLL , and proves it correct.

Translation of types

We start by translating types of ML into session types. As introduced in § 2.2, labels used for communication in translated types are based on the constructors of types: represents what happens after the initial constructor has been sent. For base types, the constructor describes already the value, hence there is nothing to be done (ie.

= 1). For non base types, this is more subtle. Given two positive session types we define their arrow as follows:

(⊕ ∈ Ret(ℓ ) • ) → := & ∈ Call(ℓ ) • ( ⊥
).

The arrow type between positive types starts with a call from context with the return values of , and then continues along ⊥ and . In particular only starts after the call message has been received. Note that this construction does not preserve positivity. With these elements in hand, we can now define and by mutual induction:

= ⊕ ∈ℭ ( ) Ret( ) • → = !( → ) = 1 ( base type) ref ref = !(get • int & & ∈N set( ) • • )
Reference types are interpreted as objects that can receive two methods calls: get and set( ) and that return the appropriate type. The interpretation of a context Δ is Δ := ⊕ ∈ℭ (Δ) Ret( ) • Δ where Δ := ∈dom(Δ) Δ( ) ( ) : for a context, all the constructors of all the parameters arrive bundled together. The interpretaton of an interface is Δ ⊢ := Δ → (a negative type).

Translation of terms

We want to translate a term Δ ⊢ : into a process ⊲ : Δ ⊢ . Doing it directly by induction would lead an inefficient translation filled with cuts that can be eliminated, as will always be of the shape & { ( ì ). } ∈ℭ (Δ) (due to the shape of Δ ⊢ ). So the primitive object for the translation of Δ ⊢

: is what comes after receiving ∈ ℭ(Δ), ie. a family of processes

( Δ ⊢ : , ⊲ Δ ⊢ ctx , )
where ∈ ℭ(Δ), is a name not present in Δ, and:

1 : 1 , . . . , :

⊢ , = 1 : 1 ⊥ ( 1 ) , . . . , 1 : ⊥ ( ) , :
. This is well-defined because for any type and compatible , both and are rooted session types. From this, we can recover the usual strategy as follows:

1 : 1 , . . . , :

⊢ : := & {Call( ) ( 1 , . . . , , ). Δ ⊢ : , } ∈ℭ (Δ) .
The interpretation is mostly straightforward and follows the usual game semantics intuition. To define the behaviour of ref(•), we need to implement a reference server, ie. a server that waits for requests (get or set) and answers appropriately, while maintaining as internal state the current value of the reference. This is done using our codereliction construct # ( ). The server accepts requests one by one, and as such is infinite. We write Proc(Γ) for the -CPO of well-typed processes

Δ, : ⊢ : , = ⊕ Ret( ( ))[ ]. [ ↔ ] ( ) Δ ⊢ : int , = ⊕ Ret( ) Δ ⊢ : bool , = ⊕ Ret( ) Δ ⊢ () : • , = ⊕ Ret() Δ ⊢ . : → , = → . ( [ := ′ ], ) ) ′ ∈ℭ ( ) Δ ⊢ : , = , ¯ , ¯ , ⊙ & Ret( ). & {Ret( )( ì ′ ). ? [ 0 ]. 0 ⊕ Call( )[ ì , ′ ]. ([ ì ↔ ì ′ ] [ ↔ ′ ] )} ⊢ plus : int → int → int (), = int •→ . ( int •→ . ( ⊕ Ret( + )) ∈N ) ∈N ⊢ equal : int → int → bool (), = int •→ . ( int •→ . ( ⊕ Ret( = )) ∈N ) ∈N ⊢ get : ref → int (), = ref → . (? [ ]. ⊕ get. & {Ret( ). ⊕ Ret( )} ∈N ) ⊢ set : ref → int → • (), = ref → . ( int •→ . (? [ ]. ⊕ set( ). & Ret(). ⊕ Ret()) ∈N ) ⊢ ref : int → ref , = int •→ . ( ⊕ ref [ ]. RefServer ( )) ∈N Shortcuts: ì → . ( ) ∈ℭ ( ) := ⊕ Ret( ). ! ( ). & { ( ì ). } ∈ℭ ( ) ⊲ : → , ?Δ
RefServer ::= fix . . # ( ). & get[ ]. ⊕ Ret( ). ( ) set( ) [ ]. ⊕ Ret(). ( )
The interpretation of typing rules for finite ML terms (ie. without fixpoint) is given in Figure 8. Recursion is simply dealt with by unfolding it. We define the -th approximant of the fixpoint operator by induction as: 0 = . . ⊥ and +1 = . . ( .

) . It is straightforward to see that ≤ +1 in Proc( ⊢ (( → ) → ( → )) → ( → ) ). Then, for any ML term , the -th approximant of , written is defined as where is replaced by . The chain ( ) ∈N is an increasing chain, hence has a least fixpoint which is the desired translation .

Translation of machines

We now define the translation of machines. As we have seen in § 2.1, the operational semantics of machines observes memory operation via labelled transitions. To model this in the world of processes, we show how to emulate these labelled transitions.

Account of visible actions. Given an alphabet Σ, we construct a session type Σ = ?⊕ ∈Σ • ok -. We translate machines to processes with a free name of type Σ . Such processes support the emission of actions in Σ as follows: . :

= ? [ ]. ⊕ . & ok.
. This allows us to define a variant of the reference server that emits a visible action at each operation performed:

RefServer ::= fix . . # ( ). & get[ ]. r ℓ, . ⊕ Ret( ). ( ) set( ) [ ]. w ℓ, . ⊕ Ret(). ( )
Unlike the previous server, this one logs (emit a visible action) everytime an action is performed. Given a state Δ ⊢ ì , we define the process

Δ ⊢ ì , = ( ¯ ) ( ì ì ¯ ) Δ , ( ∈ ì RefServer ¯ ) ( ∈dom(Δ)\ ì RefServer ¯ )
with ì ∈ dom(Δ). We only use the logging reference server for public names: every operation gives rise to a visible action. Note that the interpretation of a machine is a closed process, thus there is no need for an output channel as for the terms, as the return value is discarded. Moreover, in this case, ℭ(Δ) is a singleton, hence the parameter Δ is simply the tuple (ref, . . . , ref).

Weak bisimulation and barbed reduction-closed congruence of DiLL . On processes welltyped in the context : Σ , we can define a LTS as follows:

-→ whenever → -→ whenever ≡ . .

Using this LTS, we can define a notion of weak bisimulation on such processes.

Definition 4.1 (Weak bisimulation of DiLL ). An equivalence relation R over processes typed in the context : Σ , is a weak bisimulation if for all R with , ⊲ ∅, -→ ′ , there exists ˆ =⇒ ′ with ′ R ′ . The largest such bisimulation is called weak bisimilarity, denoted by ≈ DiLL .

Correctness of the translation

Soundness of call-by-value. We first show that our semantics is well-behaved with respect to the parallel call-by-value strategy. First, we observe that values get mapped to specific processes -those which emit a constructor right away, without interrogating the context. Formally, given a value Δ ⊢ : and given ∈ ℭ(Δ), we define ℭ( , ) ∈ ℭ( ) by induction on :

ℭ( , ) = ( ) ℭ( , ) = ℭ( , ) = ( ∈ {tt, ff, ()}) ℭ( , . ) = L 4.2. Assume Δ ⊢ : . Then Δ ⊢ : , ≡ ⊕ Ret(ℭ( , )
). for some process .

L 4.3. For Δ ⊢ : and Δ, :

⊢ : , [ / ] , ≡ [ :=ℭ ( , ) ], ⊙ ! ¯ ( ).
, .

L 4.4. Consider Δ ⊢ , : . If → , then for all , , , ≡ , . Full-abstraction on machines. We now turn our attention to the LTS on machines. We first start with a simulation lemma.

L 4.5. If Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ , then Δ ⊢ ì , =⇒ Δ ′ ⊢ ì ′ , ′ .
We now show an adequacy lemma which shows the converse. However, formulating this result is subtle due to slight differences in the LTS. In ML , operations on visible locations are performed directly as visible transitions: ⊢ :ref := 1 := 2, ↦ → 0 can do either w , 1 or w , 2 as initial transitions. In DiLL , any transition is done in two stesps: first the program connects to the memory server, which implies that a dereliction meets a codereliction; and only then the action is logged (cf. the definition of RefServer ℓ ). This means that the translation of this machine can do two -transitions, each followed by a write action. Hence, the two LTSs are not directly weakly bisimilar, but we can still show the following result:

L 4.6 (A ). If Δ ⊢ ì ,
-→ , then = , and there are two cases:

• Either Δ ⊢ ì , - → Δ ′ ⊢ ì ′ , ′ with Δ ′ ⊢ ì ′ , ′ ≡ , • Or ≡ . and Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ with Δ ′ ⊢ ì ′ , ′ ≡ .
From this, we can show that our translation preserves and reflects weak bisimulation: T 4.7 (S ). For any typed Δ ⊢ ì , and Δ ′ ⊢ ì , ′ , the following are equivalent:

(1) Δ ⊢ ì , ≈ ML Δ ⊢ ì , ′ , (2) Δ ⊢ ì , ≈ DiLL Δ ⊢ ì , ′ and (3) Δ ⊢ ì , ≅ DiLL Δ ⊢ ì , ′
From Theorem 4.7, it follows immediately that: T 4.8 (S ). For all Δ ⊢ , : , if ≅ DiLL then ≅ ML .

The converse, known as full abstraction in the denotational semantics community does not hold in general for very well-understood reasons. See the Appendix § B.4 for a counterexample. However, we still have full abstraction at second-order interfaces, cf. § 6.3.

CAUSAL GAME SEMANTICS

In this section, we describe a causal semantics interpretation of DiLL . This model interprets session types and processes as event structures, a causal model of concurrent and nondeterministic computation. The event structures denoted by session types are called games, while the event structures denoted by processes are called strategies. The contribution of this section is to extend the nonangelic model of [START_REF] Castellan | Non-angelic Concurrent Game Semantics[END_REF] with the tools for replication of [Castellan et al. 2019]. This results in the first game semantics model providing adequate modelling of nondeterministic and nonlinear languages up to weak bisimulation.

In § 5.1, we recall Winskel's event structures and introduce the notations we will be using. In § 5.2, we define the notion of games of [START_REF] Rideau | Concurrent Strategies[END_REF], as well as the interpretation of type formers on it. In § 5.3, we present strategies based on event structures of [START_REF] Castellan | Non-angelic Concurrent Game Semantics[END_REF]]. In § 5.4, we introduce composition of strategies as well as the categorical structure which is key to interpret DiLL . Finally, in § 5.5, we show problems related to replication and introduce symmetry to solve them.

Event Structures

Our model is based on event structures [Winskel 1986], introduced to give a semantic model of causal concurrency (or true concurrency). From this viewpoint, a system is a set of events along with a partial order describing the causal relationship between events; and a binary relation describing conflict (or incompatibility) between events, ie. those events that cannot occur together in the same run of the system. As a result, event structures model the system globally rather than describe independent executions. We use here prime event structures with binary conflict. Definition 5.1. An event structure is a triple ( , ≤ , #) where ( , ≤ ) is a partial order, and # ⊆ 2 is a binary irreflexive symmetric relation satisfying:

(1) [ ] def = { ′ ∈ | ′ ≤ } is finite, and (2) if # ′ and ′ ≤ ′′ then # ′′ .
Two events , ′ are in conflict when # ′ and are compatible otherwise. Two compatible events which are not ordered are called concurrent. We write ′ (immediate causal dependency) when < ′ with no events in between, and / o ′ (minimal conflict) when ( , ′ ) is the only conflicting pair in [ ] ∪ [ ′ ]. From and / o , we can recover ≤ and # via axiom (2). Depictions of event structures will use and / o . A notion of partial execution can be recoverd on event structures through the notion of configuration. Given an event structure , a configuration of is a subset ⊆ down-closed for ≤ and conflict-free. We write C( ) for the set of finite configurations of . For ∈ C( ), an extension of is an event ∈ \ such that ∪ { } ∈ C( ), which we write --⊂ .

An event structure is confusion-free when (1)

/ o ′ implies [ ] \ { } = [ ′ ] \ { ′ }
↓ def = ( , ≤ ∩ 2 , # ∩ 2 ).
Constructions on Event Structures. Given a family of event structures ( ∈ ) we define their parallel composition ∈ as follows. Its events are pairs ( ∈ , ∈ ). Causality and conflict are obtained by lifting those from the :

( , ) ≤ ( , ′ ) def = ( = ∧ ≤ ′ ) ( , )# ( , ′ ) def = ( = ∧ # ′ )
Similarly, the nondeterministic sum of the , written ∈ has the same components as ∈ except for conflict:

( , )# ∈ ( , ′ ) def = ( = ⇒ # ′ ). The empty event structure, written ∅ is the unit for both parallel composition and sum.

Games based on Event Structures

We use event structures to represent the semantic information of session types. This is a natural fit as session types feature both causality, for some messages must come before some other, and conflict, for choices are offered to both participant. In this paper, we use a simple notion of games.

Definition 5.2. A game is an event structure along with a labelling pol : → {-, +} such that:

(1) is confusion-free and race-free: ≤ ) is a forest: elements of [ ] are totally ordered by ≤ for any ∈ .

if / o ′ , then pol( ) = pol( ′ ) (2) ( ,
The first axiom comes from the local and polarised aspects of choices in session types of DiLL . Parallel composition of event structures extends to games. Given a game and ℓ ∉ , we write ℓ • , where ∈ {-, +} is a polarity, for the game prefixed by ℓ defined as follows. Its events are ∪ {ℓ}; causality is ≤ ∪{ℓ} × ( ∪ {ℓ}); and conflict is # . In general sums of games are not games as they may fail confusion-freeness or race-freeness, but the prefixed sum of games is well-defined: if is a family of games, then ∈ ℓ • is also a game (because the polarity does not depend on on ). Given a game , its dual ⊥ is the game obtained by reversing polarities in .

Moves of a game are meant to be played once, therefore to represent exponentials we need to make copies of a game to allow a move to be played several times. We define the unpolarised exponential ♯ as the infinite parallel composition ∈N . Events of ♯ are pairs ( , ) of a copy index ∈ N and an element ∈ . We sometimes write (especially in diagrams).

Examples of games related to the interpretation of ML are found in Figures 4 and5.

Strategies as Event Structures

We recall the strategies of [START_REF] Castellan | Non-angelic Concurrent Game Semantics[END_REF]]. As we have seen in § 2, the game expresses all possible behaviours allowed by the type, while the strategy selects those behaviours exhibited by the program. As a result, in a deterministic setting, a strategy on a game is actually a subset of . In general though, the strategy might make nonidempotent choices, so a strategy will be an event structure , along with a labelling function → . For the strategy to respect the rules of the game (eg. if < , then always play before ), we need the function to be a map of event structures, ensuring that every behaviour of is included in that of .

Definition 5.3. A partial map of event structures is a partial function : ⇀ such that for ∈ C( ), ∈ C( ) and which is locally injective: restricted to any configuration of is injective. We write dom( ) for the domain of , and is said to be total when dom( ) = . A map represents a simulation of by . Event structures and total maps form a category ES.

Definition 5.4. A strategy on a game is a pair ( , ) of an event structure and a partial map of event structures : ⇀ with the following properties:

Receptivity For ∈ C( ) and a negative extension of , there is a unique --⊂ with = .

Courtesy For any ′ such that and ′ are not related by ≤ (possibly because one of them is undefined), the event is not mapped to a positive move of , and ′ not mapped to a negative move of . Secrecy If / o ′ , then and ′ are not mapped to positive moves of .

Partiality allows to have internal events (akin to transitions) not corresponding to any moves of the game. An event ∈ is internal or neutral when is not defined; visible or external when it is. Receptivity ensures that a strategy cannot prevent Opponent from playing. Courtesy restricts the shape of immediate causal links in the strategy to only be from negative or neutral events to positive or neutral. Those links are asynchronous and are essential to ensure that we have a categorical identity. Finally, secrecy (together with receptivity) restricts the shape of minimal conflict: either between negative moves or between internal moves. The former are external choices (Opponent chooses) while the latter are internal choices (Player chooses).

We tend to write simply , , . . . for strategies and assume the underlying event structure is called , , ... A strategy from a game to a game is a strategy on the composite game ⊥ . We write : to distinguish them from maps. Strategies are displayed as labelled

* w ,1 * w ,2 * w ,2 * w ,1
Ret(1) + Ret(1) + Fig. 9. Nondeterministic strategy event structures, as in Figures 4 and5, which are examples of total strategies, ie. for which there are no internal moves. Because of the conflict axiom, such strategies must be also deterministic (no internal choices, only external choices). On the right, the interpretation as a strategy of the nondeterministic program ( := 1 := 2); 1 is depicted. The nondeterminism arises from a race between two writes on the same location. In this example, the map is not injective (it plays twice Ret(1)), because there might be two reasons for returning this value, depending on how the race is resolved. In the diagram, we use * for neutral events, annotated with a label describing the operation -but this information is not part of the mathematical object.

Copycat strategy. For a game , we form the copycat strategy on , : C C → ⊥ , as follows. The events of C C are exactly those of ⊥ , and

≤ C C is obtained from the transitive closure of ≤ ⊥ ∪{( , ¯ ) | ∈ ⊥
is negative} where we write ¯ ∈ ⊥ for the corresponding event to on the other side. Then

# C C ′ holds when [ ] C C ∪ [ ′ ] C C ∉ C( ⊥ )
. The labelling function is simply the identity. A strategy is negative when its minimal events are all negative. Copycat for example is a negative strategy.

The empty strategy ! A on a game is defined as the inclusion 0 ⊆ where 0 contains events ∈ such that [ ] only contains negative events (ie. it is the minimal receptive strategy).

Isomorphism of strategies. Because is arbitrary, equality of strategies is not meaningful. Rather, we consider strategies up to isomorphism. Two strategies : ⇀ and : ⇀ are isomorphic (written ) when there exists an isomorphism of event structures :

(that is a map → with an inverse map) such that • = .

Composition of strategies and categorical structure

We now explore an important algebraic structure on strategies: composition. Composition is the semantic counterpart to the operation ⊙ which connects two strategies and make them interact on a common part. Concretely, given :

and :

, we wish to define ⊙ : obtained by making and interact on and hiding the resulting interaction. This composition allows us to define a category of games and strategies. This is useful for two main reasons:

• It allows us to give a simple meaning to the restriction ( ) by simply composing with an asynchronous forwarder that connects and .

• It allows us to define the interpretation of constructs of the metalanguage by composing

with simple blocks rather than some ad-hoc construction. For instance, to interpret ⊕ ℓ. , instead of somehow prefixing by an event labelled with ⊕ ℓ, we prefer to compose by a strategy ⊕ℓ which represents an injection for a weak coproduct structure. This allows us to show the correctness of the translation by simple calculations on these little blocks rather than with an arbitrary context .

Composition of Strategies.

Composition is defined in two steps: interaction, and then hiding. Consider a strategy : from to , and a strategy : from to . We first start by forming their interaction, which is an event structure ⊛ along with a map ⊛ : ⊛ ⇀ ⊥ (during interaction, polarities on are meaningless). This event structure represents the common behaviours of and that can be reached through a common order. Intuitively, on the causal aspect, this amounts to make the union of the partial orders of and and remove cycles. This operation is somewhat involved to define concretely, but enjoys the following universal property.3 L

([C . 2018]

). There exists a unique tuple

( ⊛ , ⊛ , Π 1 : ⊛ ⇀ , Π 2 : ⊛ ⇀ ) such that
(1) If Π 1 and Π 2 are defined then (Π 1 ) and (Π 2 ) are both defined and equal (in ).

(2) Moreover, for any other tuple ( , : ⇀ , Π ′ 1 : ⇀ , Π ′ 2 : ⇀ ) satisfying the first property, there exists a unique map :

⇀ ⊛ such that Π 1 • = Π ′ 1 and Π 2 • = Π ′ 2 .
This ensures that ⊛ is well-defined up to isomorphism. The second step is to recover a strategy on ⊥ by hiding those events of ⊛ projected to . Because of secrecy, events in cannot partake in a minimal conflict, so they can be hidden without losing information up to bisimulation.

Letting be the set of events of ⊛ such that if ⊛ ( ) is defined, it is not in , we define ⊙ to be ⊛ ↓ . The map ⊛ restricts to a map ⊙ : ⊙ ⇀ ⊥ which is the composition of and . It is a strategy. . 2018]). Composition of strategies is associative, and copycat is an identity on strategies, both up to isomorphism.

For copycat to be an identity, the conditions of receptivity and courtesy are necessary. This is because composing a strategy with copycat amounts to prefixing it with an asynchronous buffer; and if the strategy is too "synchronous", this buffer may alter its observable behaviour.

Categorical structure. We define Str, the category whose objects are finite games and morphisms from to are strategies :

, considered up to isomorphism. First, duality of games extends to an isomorphism of category Str Str op : any strategy : can be regarded as a strategy ⊥ : ⊥ ⊥ . Moreover, parallel composition of games forms a monoidal structure on Str. Therefore, Str is compact-closed:

L 5.7 ([C . 2018]). (Str, , 1, (-) ⊥ ) is a compact-closed category.
Though Str does not have (co)products, it has weak (co)products. Given a family of games ( ) ∈ and of labels (ℓ ) ∈ , we define

& ∈ ℓ -• def = ∈ ℓ -• . There is a natural strategy : & ∈ ℓ -•
which plays ℓ on the right (a positive move as it is on the left), and then plays copycat between the left and the right .

L 5.8. For every family of strategies ( :

) ∈ there exists a strategy ∈ : & ∈ ℓ -• such that ⊙ ∈
By duality, we get weak coproducts:

⊕ ∈ ℓ + • def = ∈ ℓ + • , and define def = ⊥ : ⊕ ∈ ℓ + • .
These are used to interpret the additive fragment of the metalanguage.

Replication and symmetry

We have weak co-products, and compact-closedness so we can interpret a large part of DiLL . For exponentials, we would be tempted to use ♯(-) construction to interpret !(•) and ?(•). However, for the interpretation be to sound, we would require special structural morphisms. It is well-known from the Linear Logic categorical semantics [START_REF] Melliès | Categorical semantics of linear logic[END_REF]] that we would need ♯(-) to have a (co)monadic structure to be able to interpret correctly the promotion, and dereliction rule.

There are natural candidates for a monad structure on ♯(-):

: ( ∈ ) ↦ → (0, ) ∈ ♯ : ( , ( ,
)) ∈ ♯♯ ↦ → ( , , ) ∈ ♯
These can be lifted to strategies, however one can see already in ES those do not satisfy the monadic laws: indeed • : ♯ → ♯ sends ( , ) to ( , 0 , ) which may not be the same as ( , ).

Event Structures with Symmetry. The solution to this problem is to relax the notion of equality to be up to copy indices. This intuition is formalised through event structures with symmetry:

Definition 5.9. An isomorphism family on an event structure is a family ˜ of order-isomorphisms :

with , ∈ C( ) such that

(1) ˜ contains all identities, and is stable under inverse and composition (2) If ⊆ ′ and : ′ ′ ∈ ˜ , then | : ∈ ˜ (3) If ⊆ ′ and :

∈ ˜ , then there exists a (non-necessarily unique) ′ ∈ C( ) such that extends to ′ : ′ ′ ∈ ˜ .

An event structure with symmetry is a pair ( , ˜ ) of an event structure and an isomorphism family ˜ on . We write E, F , ... for event structures with symmetry.

Most constructions on event structures (such as parallel composition, sum, prefixing) can be extended seamlessly to event structures with symmetry [Winskel 2007]. The main purpose of these objects is to support a weaker equivalence relation on maps. Consider two partial maps , : ⇀ between event structures and an isomorphism family ˜ on . These maps are similar wrt ˜ , written ∼ ˜ when for all ∈ C ( ), the mapping ↦ → defines a bijection which is in ˜ . When the family is clear from context, we write ∼ . Now, we can extend the ♯(-) construction to work at the level of symmetry. Given an event structure with symmetry E, define an isomorphism family ♯ ˜ on ♯ containing all the : for which there exists : N → N such that (1) for ( , ) ∈ , ( , ) is of the form ( , ′ )and(2) {( , ′ ) | ( , ) = ( , ′ )} ∈ ˜ . We define the event structure with symmetry ♯E as (♯ , ♯ ˜ ). The induced equivalence formally captures to be equal "up to copy indices".

A map of event structures with symmetry :

E ⇀ F is a map : ⇀ such that for all ∈ ˜ , def = {( , ′ ) | ( , ′ ) ∈ } is in ˜ .
Event structures with symmetry and total maps form a category ESS. Winskel [2007] proved that ♯(-) : ESS → ESS is a monad up to ∼.

Thin concurrent games with symmetry. Simply equipping games with one symmetry works [START_REF] Castellan | Symmetry in Concurrent Games[END_REF]] but leads to a setting uncomfortable for semantics. We follow here [Castellan et al. 2019] and add three symmetries on games: one global symmetry, and one subsymmetry for each player. (Details of this section appear in the unpublished thesis [START_REF] Castellan | Concurrent structures in game semantics[END_REF]).

Definition 5.10. A thin concurrent game (tcg) is a tuple A = ( , ˜ , ˜ + , ˜ -) where is a game, and ˜ , ˜ + , ˜ -are isomorphism families on subject to axioms listed in [Castellan et al. 2019]; in particular ˜ -and ˜ + are sub-isomorphism families of ˜ .

The intuition is that ˜ -(resp. ˜ + ) contains only isomorphisms that affect negative (resp. positive) events. This idea of polarised decomposition of the symmetry was first introduced by [START_REF] Melliès | Asynchronous games 1: A group-theoretic formulation of uniformity[END_REF] in a simpler setting. Game operations (parallel composition, dual, prefixed sums) extend to tcgs.

However, in general ♯A is not a tcg even if A is. It only works for polarised games: a game is negative (resp. positive), when all its minimal events are negative (resp. positive). A game is polarised when it is either negative or positive.

L 5.11 ([C . 2019]).

If A is a polarised tcg, then ♯A can be made into a tcg.

A negative symmetry in ♯A leaves positive copy indices unchanged, and conversely for positive symmetries. Since the interpretation of session types is not polarised, we need to explicitly lift them before using ♯(-): indeed a lifted game is always polarised as it has a unique minimal event. Depending on the polarity of the minimal event, we get the two exponentials. We define:

!A = ♯(Req -• A) ?A = ♯(Req + • A).
Uniform Strategies. Symmetry on games induces naturally an equivalence relation on strategies, relaxing isomorphism by asking that the triangle commutes up to symmetry on the game. This equivalence, however, is not a congruence since nothing prevents a strategy from observing copy indices from Opponent. To recover a well-behaved compositional setting, we need to ensure that the strategy we consider behaves uniformly with respect to copy indices from Opponent. It turns out that we need to add extra structures on strategies, under the form of an isomorphism family.

Definition 5.12. Consider a tcg A. A uniformity witness for an essential strategy : ⇀ is an isomorphism family ˜ on such that:

(1) becomes a map of event structures with symmetry ( , ˜ ) → ( , ˜ );

(2) if :

∈ ˜ and extends to : ′ ′ ∈ ˜ with ⊆ -′ , then extends to a ′ such that ′ = ; (3) if :

∈ ˜ is the identity on negative elements of , then is the identity on .

A uniform strategy on A is a strategy on along with a uniformity witness for .

We can lift the equivalence relation ∼ from maps to strategies: two uniform strategies : → and : → are weakly isomorphic (written ≅ ) when there exists an isomorphism of event structures with symmetry : S T such that • ∼ .

T 5.13 ([C 2017]). Uniformity witnesses compose and weak isomorphism is a congruence on uniform strategies. As result, tcgs and uniform strategies up to weak isomorphism form a compact-closed category UStr.

The weak products of Str induce weak products in UStr in a straighforward manner. We also get the desired In this settting, we get the desired (co)monadic structure: L 5.14. The construction !(-) extends to an exponential comonad UStr → UStr, that is it comes equipped a functorial action plus the following strategies:

return: d A : !A A digging: A : !A ‼A contraction: c A : ! ! ! .
satisfying standard laws [START_REF] Melliès | Categorical semantics of linear logic[END_REF]].

Recursion. We finish by detailing the structure in UStr to interpret infinite processes. An embedding of into (both strategies on A) is a map : S → T such that • ∼ and such that restricted to its image defines an isomorphism. We write : ↩→ . This notion is useful to define the meaning of infinite objects by taking a limit of increasing strategies.

L 5.15. Any countable chain of embeddings ( : ↩→ +1 ) ∈N has a colimit, ie. there exists a unique a strategy and embeddings : ↩→ such that +1 • = .

INTERPRETATION OF DiLL INTO STRATEGIES

We are ready to interpret DiLL into UStr. In § 6.1, we show how to interpret session types and processes. In § 6.2, we prove that the interpretation is fully abstract with respect to a weak bisimulation on strategies. Finally, in § 6.3 we discuss the resulting causal semantics of ML .

Semantics interpretation

Interpretation of types. The interpretation of types is straightforward, since we have seen the semantic constructions corresponding to type formers in § 5: ! = ! , ? = ? ,

1 . . . = 1 . . . , & ∈ ℓ -• = & ∈ ℓ -• and ⊕ ∈ ℓ + • = ⊕ ∈ ℓ + • .
Minimal events of are either of the form ℓ ∈ L (a label) or Req for starting new requests. A session type is rooted if and only if all minimal events of are in conflict. The interpretation of contexts is a simple parallel composition: 1 : 1 , . . . , : = 1 . . . . Minimal events of Δ are of the form ( , ) where ∈ dom(Δ) and is the minimal event of Δ( ) .

Interpretation of terms. To interpret terms, we make use of the categorical structure presented in § 5. In particular, if ì :: is defined, then there is an isomorphism ì :: : ì :: obtained from the monoidal structure. Given an isomorphism : A B between tcgs, and : A a uniform strategy, we write * ( ) : B for the reindexed strategy on B.

What remains to be constructed in the semantic world is how to interpret codereliction, ie. how to introduce nondeterminism and races. Such a construct is interpreted in UStr through a morphism ¯ : ! ! .

! → ! Req - Req - * * Req + , Req + , a - a, + a, +
a, , -a, , - a, , + a, , + Fig. 10. Strategy ¯ for = a +

The intuition is that requests on the right side race to get forwarded to ; requests that did not win the race are then forwarded to the left ! . Since this strategy has a complex operational behaviour, let us start by an informal description, based on the example where the game has a single positive move, ie. = + . The desired strategy ¯ for a single move game = a + is (partially) depicted in Figure 10. The strategy starts by waiting for a request on the rightmost ! . The different Req -are all racing together to be considered the first message acknowledged by ¯ . Hence, one neutral event per Req -is triggered when the th message wins the race. If the th message has won, then the copy of on the left is put in contact with the successor of Req -, expressed by the links - , + and * , + . Then, if has won the race, it means that any other ≠ lost. In that case, messages on the component are forwarded to the leftmost ! : Req - Req + , and * Req + , . From there, we have a copycat strategy between the th copy of on the left and on the right. Formally, the event structure is defined as follows. Events are of one of the following form:

0 ⊲ Δ = ! Δ ⊲ ?Γ, Γ 1 ⊲ ?Γ, Γ 2 ⊲ ?Γ, Γ 1 , Γ 2 = ⊙ ( ) ∈ ⊲ Γ, ì :: ⊕ ℓ [ ì ]. ⊲ Γ, : ⊕ ∈ ℓ • = ( : ⊕ ∈ ℓ • ) ⊙ ( * ì :: ( ) : Γ ⊥ ) ∀ : , ⊲ Γ, ì :: & {ℓ ( ì ). } ∈ ⊲ Γ, : & ∈ ℓ • = * ì :: ( ) : Γ ⊥ ∈ ⊲ : , : ⊥ , Γ ( : ) ⊲ Γ = ( : ( ⊥ ) Γ ) ⊙ ( : ∅ ⊥ ) ⊲ ?Γ, ì :: ! ( ì ). ⊲ ?Γ, : ! = (! * ì :: ( ) : !! Γ ⊥ ! ) ⊙ Γ ⊥ ⊲ Γ
• an event Req -for ∈ N mapped to the initial move of the right ! ;

• an internal event * , representing the fact that the th request has won the race • an event Req + , for ≠ , corresponding to the forwarding of Req -when wins the race; • an event , for every ∈ C C and ∈ N representing the forwarding to when the race is won by ; • an event , , for every distinct numbers , ≠ N and ∈ C C , for forwarding the th copy to ! when loses the race to .

Causality includes the usual causal order on the copies of C C , plus the following links: might not be receptive if is positive (as in the example), so that the strategy ¯ is obtained by precomposing with copycat to ensure receptivity. The interpretation of finite processes is given in Figure 11. Infinite processes are obtained as limits of chain of interpretation of their approximants, since the interpretation is easily seen to be monotonic.

We start by showing the adequacy of our translation. To state it, we need a notion of transition on strategies. Event structures come with a natural notion of transition system, given by configurations. Given an event structure and ∈ C( ), we define / as featuring those events ∈ \ that are not in conflict with any events in , with causality and conflict directly inherited from . This can be lifted to the level of strategies. Given a uniform strategy : ⇀ A, and a configuration ∈ C( ), we build the uniform strategy / : S/ ⇀ A/ (read after ). We say that : can do a transition to with visible actions ∈ C( ), written y ---→ , when there exists a configuration ∈ C( ) such that / ≅ and in ˜ . The particular case where = ∅ corresponds to an internal transition and is simply written --→ .

Full Abstraction

Using the notion of transition on strategies defined in the previous section, we define weak bisimulations between strategies: Definition 6.3. A weak bisimulation is an equivalence relation R between uniform strategies on the same tcg such that if R , for all configuration ∈ C( ), if ---→ ′ , then there exists ′ such that ---→ ′ with ′ R ′ . We write ≈ for the largest weak bisimulation. L 6.4. Weak bisimilarity is a congruence (stable under composition), hence ≅ implies ≈ .

From this result, and using the standard method of action testers [START_REF] Hennessy | A Distributed Pi-Calculus[END_REF]], we derive: T 6.5 (S F A ). Consider , ⊲ Δ. Then we have ≅ DiLL iff ≈ .

Causal Semantics of ML

By composing the syntactic translation and the semantics interpretation, we get an interpretation of types and programs of ML in terms of event structures: = and = . From the previous results, we immediately get: L 6.6 (A ). Consider two terms Δ ⊢ , : . If ≈ , then ≅ ML .

As we discussed in § 4.4, the converse does not hold (see Appendix B.4). However, we have second-order full abstraction. An interface Δ ⊢ is second-order when (1) is a base type and (2) types in Δ are either base types, or arrow types between base types. We have: T 6.7 (F A ). Consider two terms , well-typed on a second-order interface Δ ⊢ . Then ≅ ML if and only if ≈ .

This theorem is useful when applied to first-order functions calling other external first-order functions (from say, libraries).

IMPLEMENTATION

To illustate the causal model, we have used the model presented in this paper to implement a causal interpretation of a subset of OCaml corresponding to ML into event structures, representing strategies. The metalanguage process is built implicitly but not explicitly represented as they are not very informative and extremely verbose. The (anonymised) prototype is a web application, available at: http://programminggamesemantics.github.io/index.html

The prototype allows entering OCaml code restricted to functions, product, record types and sum types. The standard library of OCaml is replaced by a simple kernel implemented by specific strategies to represent integer references (called var) and parallelism. See the webpage for details. The event structure is not displayed in its entirety as it would often be infinite (because of infinite datatypes and recursion) but instead the user can explore interactively branches of the computation they are interested in by clicking on Program events to unlock the next step of computation.

RELATED WORK

Metalanguage and Process Representation for Strategies Games. [START_REF] Hyland | Pi-Calculus, Dialogue Games and PCF[END_REF] first studied a relationship between game semantics and the -calculus, where -calculus processes are used to denote plays of innocent strategies (for PCF). This idea led to recast the traditional encoding of the call-by-value -calculus into the -calculus [Milner 1992b] into a game semantics model for call-by-value PCF [START_REF] Honda | Game-Theoretic Analysis of Call-by-Value Computation[END_REF]. In the sequential setting, the work by [START_REF] Longley | Some Programming Languages Suggested by Game Models (Extended Abstract)[END_REF] proposed a programming language to describe sequential innocent strategies as a whole. Later, [START_REF] Goyet | The Lambda Lambda-Bar calculus: a dual calculus for unconstrained strategies[END_REF] proposed an abstract calculus for sequential strategies, close to the I-calculus. [START_REF] Dimovski | CSP Representation of Game Semantics for Second-Order Idealized Algol[END_REF]; [START_REF] Ghica | Compositional Model Extraction for Higher-Order Concurrent Programs[END_REF] represent strategies as CSP terms for use with model checkers, but CSP is only used a way to represent strategies, rather than a target language for syntactic translations -in particular all reasoning must be done at the level of the model. In a similar vein, [START_REF] Disney | Game Semantics for Type Soundness[END_REF] argue for a reading of strategies in terms of processes in the sequential setting, for type soundness.

Game Semantics for Concurrency and Nondeterminism. The first concurrent game semantics model, based on traces, is due to [START_REF] Laird | A Game Semantics of Idealized CSP[END_REF] for a message-passing language, extended to call-by-name shared-memory later by [START_REF] Ghica | Angelic Semantics of Fine-Grained Concurrency[END_REF], angelic models which are fully abstract for may-equivalence. Causal models arrived later with [START_REF] Sakayori | A Truly Concurrent Game Model of the Asynchronous -Calculus[END_REF] (asynchronous -calculus) and [START_REF] Castellan | Causality vs interleaving in game semantics[END_REF] (IPA: call-by-name shared-memory), which are both angelic (ie. only adequate for may-testing). [START_REF] Harmer | A Fully Abstract Game Semantics for Finite Nondeterminism[END_REF] provide the first non-angelic model of game semantics in the sequential setting based on stopping traces. This approach is tailored to must-equivalence.

Our approach thus gives the first non-angelic game model of a realistic higher-order concurrent programming language, capturing faithfully the nondeterministic branching behaviours of sharedmemory concurrent programs.

Recently, [START_REF] Melliès | Template games and differential linear logic[END_REF] gave a games semantics model for DiLL based on templates games. It differs from ours in two ways: (1) his model is synchronous, while our model is asynchronous (due to courtesy); and (2) it ignores deadlocks, preventing from modelling ML adequately. [START_REF] Melliès | Concurrent separation logic meets template games[END_REF] extended it later to model Concurrent Separation Logic.

Extensions of the Linear-Logic and Session Types Correspondence. In this paper, we use a variation of Differential Linear Logic (DiLL) to express nondeterminism built on deterministic computations. [START_REF] Beffara | A Concurrent Model for Linear Logic[END_REF] presents a model of Linear Logic in terms of processes of the I-calculus, used to interpret concurrent extensions of the -calculus. In the context of proof-nets, [START_REF] Ehrhard | Interpreting a Finitary Pi-Calculus in Differential Interaction Nets[END_REF] investigate encoding a finitary -calculus in a transition system of labelled differential interaction nets.

Following the work by [START_REF] Toninho | Functions as Session-Typed Processes[END_REF] on an encoding of the simply-typed -calculus, [START_REF] Toninho | On Polymorphic Sessions And Functions: A Tale of Two (Fully Abstract) Encodings[END_REF] have proven that there exist mutually inverse and fully abstract encodings between a polymorphic session -calculus in [START_REF] Caires | Behavioral Polymorphism and Parametricity in Session-Based Communication[END_REF]] and a linear formulation of System F. To gain expressiveness beyond functional and strong normalising behaviours, several extensions have been proposed, eg. the lock primitives for nondeterminism [START_REF] Balzer | Manifest sharing with session types[END_REF]; dynamic monitoring [START_REF] Gommerstadt | Session-Typed Concurrent Contracts[END_REF][START_REF] Jia | Monitors and Blame Assignment for Higher-order Session Types[END_REF]; exceptional handling [START_REF] Caires | Linearity, Control Effects, and Behavioral Types[END_REF]; multiparty interactions [START_REF] Carbone | Coherence Generalises Duality: a logical explanation of multiparty session types[END_REF][START_REF] Carbone | Multiparty Session Types as Coherence Proofs[END_REF]; hyperenvironments to capture non-blocking I/O [Kokke et al. 2019a]; and a bounded linear logic based-extension to model racy conditions [Kokke et al. 2019b]. [START_REF] Balzer | A Universal Session Type for Untyped Asynchronous Communication[END_REF] show an encoding of untyped asynchronous communication in [START_REF] Balzer | Manifest sharing with session types[END_REF], and [START_REF] Balzer | Manifest Deadlock-Freedom for Shared Session Types[END_REF] successfully enabled deadlock-freedom by introducing extra-logically imposed partial orders.

Our approach differs from them, aiming to describe game semantics translations more accurately by the metalanguage arisen from event structures grounded on DiLL. None of the above calculi provides a fully abstract encoding from nondeterministic and concurrent languages (ie. ML ) nor a causal semantic interpretation.

CONCLUSION

Our contribution in this paper is twofold: we have presented a factorisation of the usual game semantics methodology in two steps: (1) a syntactic translation and (2) a semantics interpretation which allows for separating concerns when designing new game semantics models. We have applied this methodology to build the first non-angelic interactive model of a call-by-value language with shared memory concurrency. We have used our framework to implement a causal modelling of a subset of a concurrent extension of OCaml. We believe our methodology proves promising to model mainstream programming languages and systems where semanticists will need inputs from language or system designers who do not have an immediate access to game semantics.

Another avenue would be to use the model to reason about open terms, and inserts itself naturally in some new research programs such as [START_REF] Gu | Certified Concurrent Abstraction Layers[END_REF][START_REF] Koenig | Refinement-Based Game Semantics for Certified Abstraction Layers[END_REF]] which aim at building large certified systems by assembling components proved correct in isolation.

Other future work include relaxed shared memory using the techniques presented in [START_REF] Castellan | Weak memory models using event structures[END_REF]], and trying to characterise UStr (or a subset of it) as an initial category.

• If it is a conditional if ′ , then must be normal as otherwise would not be normal. If was a value, then it would have to be an immediate boolean since semiclosed terms do not have free variables of type bool. But then, would reduce to or ′ , which is absurd. So must be stuck.

• If it is a variable: impossible, variable are values.

• If it is application: then has the form 1 . . . where is not an application. Since is semiclosed, can only be an abstraction or a constant.

-If it is an abstraction: then all the must be in normal form. Moreover, the first argument must not be a value otherwise, there would be a reduction.

-If it a constant, then we see that the only possible cases are ref( ), ! , or := . • Either Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ with Δ ′ ⊢ ì ′ , ′ ≡ , • Or ≡ . and Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ with Δ ′ ⊢ ì ′ , ′ ≡ .

P

. First, by Lemma 4.4, we can assume without loss of generality that is in normal form. Moreover, given the shape of Δ ⊢ ì , it is clear that must be as there are no visible actions at top level. By Lemma B.2, we know that must be stuck. We examine the cases given by Lemma B.1:

• If = ref( ), then we have a contradiction as this term cannot reduce.

• The cases for ! , are := are straightforward calculation. For instance, assume that = ! . In this case, there are only two possible reductions: indeed , starts with a dereliction that has to communicate with the codereliction on . That must have caused the -transition. Then there are two cases, whether ∈ ì or not.

-If ∉ ì : then the read is performed, and the value is sent back to , and we have ≡ Δ ⊢ ì ( ), as desired. -Otherwise, is visible and there is a visible transition on in front of the continuation, and we end up on the same process after performing it.

• If = if 0
′ , then we know that 0 must be stuck. By construction of the translation, we must have Δ ⊢ ì 0 , -→ ′ and can be obtained from ′ by the interpretation of if.

Then we can apply the induction hypothesis. • If = ( ì . 0 ) ì : then once again by the definition of the interpretation the reduction must occur within one of the , and we conclude by induction.

B.3 Conclusion

We can now conclude the adequacy result and the correctness result of our translation of machines.

L 4.6 (A

). If Δ ⊢ ì , -→ , then = , and there are two cases:

• Either Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ with Δ ′ ⊢ ì ′ , ′ ≡ , strategies. Duality induces an isomorphism (UStr -) op UStr + . This operation on tcgs extends to a functor ↑ --: UStr → UStr -: given : A B, ↑ -starts by acknowledging the negative Req - on the right, before playing Req + on the left, and continuing as . As a result, ↑ -is a negative strategy.

L

C.1. The functor ↑ -(-) : UStr → UStr -is a right adjunt to the inclusion UStr -⊆ UStr.

P

. The adjunction is fairly simple to describe: • From : ↑ + in UStr + , by removing the initial negative event on ↑ + , we get a strategy in UStr (not necessarily negative).

• From :

in UStr, we can build a strategy Req -• : ↑ + which is well-defined because is positive.

It is clear that these operations are inverse of each other; naturality is a simple calculation.

Lifting the monad. We are now ready to prove the result: satisfying standard laws [START_REF] Melliès | Categorical semantics of linear logic[END_REF]].

P

. From [START_REF] Castellan | Concurrent structures in game semantics[END_REF]], we know that ♯• is an exponential comonad on UStr -. We notice that ! = ♯↑ -A and we conclude by the fact that ↑ -A is a right adjunct to the inclusion: it thus transports exponential comonads on UStr -to exponential comonads on UStr as desired.

P .

(1) To show the result on ≡, since ≅ is a congruence, it is enough to show that it satisfies the rules listed in Figure 7. The first block is a consequence of the monoidal structure and the compact-closure. The third block is a direct consequence of the weak product structure and the exponential comonad structure. For the second block:

• [ ]: In the composition induced by ( ), the initial move is a negative move on . That means that every positive move will be dependent on this negative move, in particular any positive move. This means that the composition can only contain negative events on channels distinct to , , so the process must be isomorphic to the empty strategy. If ≠ { , }, then we can safely push it outside the restriction: indeed, this will not create new causal links from the prefix on to positive actions in : such actions are already waiting on . Hence, they are waiting on an action on , that if happens, must occur in -[ ], hence after -.

Fig. 1 .

 1 Fig. 1. An overview of the methodology on an example

Fig. 6 .

 6 Fig. 6. Typing rules of the metalanguage

Fig. 7 .

 7 Fig. 7. The structural congruence rules and reductions for DiLL

  ∈ N | () | tt | ff | | ref label: ℓ ::= Call( ) | Ret( )We often abbreviate Call(()) and Ret(()) as Call() and Ret(). A type of ML will be interpreted as a positive session type of the form ⊕ ∈ℭ ( ) Ret( ) •. Positive types are adequate to model callby-value reduction as the initial positive move is used to tell Context that the term does converge to a value. The session type

Fig. 8 .

 8 Fig. 8. Interpretation of ML into the metalanguage on Γ. In particular, the least element of Proc(Γ) is 0. We then define the server via a least fixpoint of a function on the -CPO Proc( : ref ref )) N (ordered pointwise) as follows:

  and (2) the relation ( / o ∪ = ) is an equivalence relation. Its equivalence classes are called cells. Confusion-free event structure have local nondeterminism and cells represent choices between different branches of the program. Finally, given a set ⊆ , the projection of to is the event structure

  Fig. 11. Interpretation of DiLL into Str

L 6. 1 .

 1 Consider ⊲ Δ. (1) (a) If ≡ , then ≅ ; and (b) If → then --→ (2) If ≡ ⊕ ℓ [ ì ]. , then there exists ∈ min( ) mapped to ( , ℓ) and /{ } ≅ . (3) If ≡ ? [ ì ]. , then there exists ∈ min( ) mapped to ( , Req) and /Consider a process ⊲ Δ. We have: (1) If --→ , then there exists ⊲ Δ with → * and ≅ . (2) If ∈ is a minimal positive event mapped to ( , ) ∈ Δ then (a) if = Req, then ≡ ? [ ì ]. and ≅ /{ }; and (b) if = ℓ, then ≡ ⊕ ℓ [ ì ]. and ≅ /{ }.

B. 2

 2 Finite adequacy L B.2. For any semiclosed value , Δ ⊢ ì , cannot do any transition. P . Easy inspection. L B.3 (F ). Consider a finite machine Δ ⊢ ì , . If Δ ⊢ ì , -→ , then = , and there are two cases:

L 5 .

 5 14. The construction !(-) extends to an exponential comonad UStr → UStr, that is it comes equipped a functorial action plus the following strategies:return: d A : !A A digging: A : !A ‼A contraction: c A : ! ! ! .

  (a) If ≡ , then ≅ ; and (b) If → then --→ (2) If ≡ ⊕ ℓ [ ì ]. , then there exists ∈ min( ) mapped to ( , ℓ) and /{ } ≅ . (3) If ≡ ? [ ì ]. , then there exists ∈ min( ) mapped to ( , Req) and /{ } ≅ .

  • [ ]: Consequence of compact closure • [ ]: Consequence of the categorical setting: the forwarder behaves as an identity • [ ]:

  communication from Context to Program and from Program to Context. Since there are only two participants, we choose to describe the protocol from the point of view of Program: the first kind

		: bool ⊢ bool		neg
		Call(tt) -	Call(ff) -		Call(tt) -	Call(ff) -
	Ret(tt) +	Ret(ff) +	Ret(tt) +	Ret(ff) +	Ret(ff) +	Ret(tt) +
	Fig. 4. Semantics interpretation of the negation: game (le ) and strategy (right)

  Our viewpoint is that each reference has an owner -the one that declared it with ref, and when an open program has a free variable of type ref, it

is not the owner of the reference, but Context is. Operations on non-owned references are simply forwarded to the owner: if a term has a free reference , then what it receives from Context is simply a name at which it can send the memory operations. In our simple setting, there are only two operations: get and set. For instance, : ref ⊢ :=! +1 : • will be interpreted as a process that does two requests on the object : a get, and then a set. Dually, when interpreting the construct ref(•), Program is the owner, and Context is the user (since the reference is returned to Context): this means that Program must create a server that can adequately handle these requests.

  Conflict is generated by asking that the * are all in mutual conflict.

	• Req -	* and * ≤ , for all ∈ C C ;
	• Req -	Req + , and *	Req + , for any ≠ : Req + , is played when Opponent made the -th
	request and won the race; and
	• Req + , ≤ , , for ∈ C C .

It differs from DILL (dual intuitionistic linear logic) in[Caires and Pfenning

2010].

The distinction in Linear Logic is crucial to ensure deadlock-freedom and hence cut-elimination. Since programs of ML do have deadlocks, we explicitly want to identify the multiplicative connective.

In the case without internal events, this is a pullback, but in this setting, the pullback exists but does not capture the right operational intuitions.

Glynn Winskel. 1986. Event Structures. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986. 325-392. https

Then by the intervion of [ ], we have:

⊲ Γ 1 , ?Γ 0 , :? and # ( ì ). ⊲ Γ 2 , ?Γ 0 , : ⊥ and ⊲ Γ 3 , ?Γ 0 with Γ = Γ 1 , Γ 2 , Γ 3 , ?Γ 0 (2) From ( 2), and inversion of [ ] and [ ], we have ⊲ Γ 1 , ?Γ 0 , :? , ì :: and ⊲ Γ 2 , ?Γ 0 , : ⊥ , ì ::

From (3), applying [ ] and [ ], we have

Applying [ ] to (4) and (2), we have:

Applying [ ] to (5), we obtain the result.

Case (2: [ ] and [ ]))

Straightforward by IH.

B PROOFS OF § 4

We prove here Theorem 4.7.

B.1 Approximation and normal form

Consider a finite semiclosed term . Because there are no fixpoint, we know that must reduce to a normal form nf( ) for → (since we are simply in the simply-typed -calculus with uninterpreted constants). By Lemma 4.4, we know that , ≡ nf( ) , . A term is stuck when it is in normal form but not a value. Any finite term has a normal form written nf( ). We say that a machine is finite when the term it contains is finite. In that case, we extend the notation nf(

If is a base type, we write nf( ) for the set of normal forms of semiclosed terms of type .

L

B.1. The set of semiclosed stuck terms is contained in the following grammar:

where means any term, and means normal form (not necessarily stuck).

P

. Consider a stuck term . We proceed by induction on its syntax. • It cannot be a -abstraction since semiclosed terms do not have arrow types.

• Or ≡ . and Δ ⊢ ì , -→ Δ ′ ⊢ ì ′ , ′ with Δ ′ ⊢ ì ′ , ′ ≡ .

P

. Write for the input machine. Clearly = for the same reason as in Lemma B.3. Consider now a finite approximation 0 of : by definition of the LTS, there exists a finite approximation 0 of with 0 -→ 0 . By continuity, we can find a finite approximation of such that

. Then, we can apply Lemma B.3, and do a case distinctionthe two cases are similar. Say that

Then it is easy to see that Δ ′ ⊢ ì ′ , ′ is the limit of the Δ ′ ⊢ ì ′ , ′ , hence Δ ⊢ ì , ≡ as desired.

T 4.7 (S ). For typed Δ ⊢ ì , and Δ ′ ⊢ ì , ′ , the following are equivalent:

are weak bisimulations.

(1) For R 0 :

) ∈ R 0 , then it is easy to see that they both can only do before getting to ( ,

, then we know that = by Lemma 4.6, and there are two cases:

-If -→ ′ with ′ ≡ , then -→ ′ for some ′ with ′ ≈ ML ′ and we conclude via Lemma 4.5.

-If -→ ′ and ′ ≡ . , then -→ ′ with ′ ≈ ML ′ . By Lemma 4.5, we know that -→ and ≡ . ′ hence ( , ) ∈ R 0 as desired.

(2) For R 1 : Assume that ( , ) ∈ R 1 , and -→ ′ . Then by Lemma 4.5, we have =⇒ ′ .

By construction, this implies that =⇒ ′ for some ′ , and we conclude by Lemma 4.6.

(2) ⇔ (3) For this, we need the full abstraction result of Theorem 6.5. Indeed, it is easy to see that machines , ′ , we have

B.4 Discussion on full abstraction

In this subsection, we offer a detailed discussion on the full abstraction. This is a well-known phenomenon in game semantics due to some information that is lost during the translation: the difference between calling and returning. At the level of the metalanguage, the distinction is gone which allows us to write contexts that can for instance, evaluate an argument and return in parallel which is not possible in ML . We now show a concrete examples, using the following two terms:

( . := 1; := 1); :=! + 1; if(! = 1 and ! = 0) then () else ⊥ and are higher-order terms, with one higher order parameter : (• → •) → •. calls its parameter on a dummy function, and then diverges. does almost the same, except that there is a possibility for it converge: if at the end, equals one and zero. From the point of view of Context, the two arguments are equivalent, as they always return after being called. For to converge, only must be set to one, which is impossible to achieve using a context written in ML as calls to will always finish completely before the control is passed back to . However, there is a process that can interact differently with and . Indeed, their interpretations at are processes over the context Γ = : Ret() + , : ?(Call( ) + • (!Call() -• Ret() + Ret() -)) On this interface, we can build a context that will trigger the events Call() -and Ret() -in parallel, which simulates a function that calls its argument while returning. In , this triggers several races, including one between the write on and the read on : this race makes it possible for the condition to be evaluated after is set to one, but before is. Such a context can be written as follows:

However as noted in the main part of the paper, we can derive the full abstraction result for the second-order (Theorem 6.7).

C PROOFS OF § 5 L 5.15. Any countable chain of embeddings ( : ↩→ +1 ) ∈N has a colimit, ie. there exists a unique a strategy and embeddings : ↩→ such that +1 • = .

P

. Write for the underlying event structure of . We define

with the convention that 0 ( 0 ) = ∅. Causality is defined as follows: ≤ ′ when there exists ∈ N where both , ′ can be embeded and where ≤ ′ . Similarly for conflict. It is easy to see that embeds into and that is the smallest such event structure. Moreover, we can project to by simply using the .

L 5.8. For every family of strategies ( :

Without loss of generality, we can assume that each contains the minimal strategy on ⊥

. We define to be the union of the , plus events {ℓ | ∈ }, with all courteous links from ℓ to events in , and conflict that of the plus all the minimal conflict between the ℓ . The mapping from to ⊥ & ∈ ℓ -• is given by the . It is easy to check that this strategy satisfies the desired axiom.

C.1 Proof of the linear exponential comonad

Lifting and polarised categories. We define two operations on game: ↑ + A = Req + • A and ↑ -A = Req -• A. We define the polarised subcategories of UStr: UStr -is the category of negative games and negative strategies; while UStr + is the category of positive games and negative #( ì ) ) → ( ) ( ( ì ì ) ( )), then the Req + emitted by the dereliction meets one initial Req -of the codereliction. This synchronisation is internal and unlocks the desired neutral event * . Then, behaves as copycat, which are the counterpart of the restrictions appearing in the right-hand-side of the syntactic rule. (1) This reduction can be already be done by a finite approximant 0 of : 0 → 0 and finite approximation of . We can proceed by induction on 0 .

• If 0 = 1 2 : then the neutral event must come from 1 or 2 , and we can conclude by induction.

• If 0 starts with a negative prefix, then it does not have a neutral minimal event.

• If 0 starts with a positive prefix, we conclude by induction.

• If 0 is of the form ( ì ì ) 1 : we consider the neutral event of 0 . It corresponds to a neutral event ′ of 1 which might not be minimal. Without loss of generality, we can assume that all deterministic reductions in 1 are reduced. This means that 1 must be of the form #( ì ) | ? ¯ [ ì ]. where and ¯ are connected by a nu, and we can conclude.

(2) Same reasoning, by induction on a finite approximant.

D.2 Proof of full abstraction T 6.5 (S F A ). Consider , ⊲ Δ. Then we have ≅ DiLL iff ≈ .

P

. From Lemmata 6.4, 6.1, and 6.2, we get easily the right-to-left direction. For the left-to-right direction, we use action testers. We show that R = {( , ) | ≅ DiLL } is a weak bisimulation.

• Assume that --→ , then we directly apply adequacy and the definition of ≅ DiLL to conclude.

• Assume that -----→ , then we can conclude by receptivity.

• The interesting case is when Then we consider the context:

We have [ ] ≡ 0 and [ ] ≡ 0 . Hence, because ≅ DiLL is a congruence, we have that 0 ≅ DiLL 0 as desired.

-If = Req, then the reasoning is the same.

D.3 Second-order full abstraction

We now show Theorem 6.7. P . We only need to show the left-to-right inclusion. By Lemma D.1, we can assume that Δ only contains function types, ie. Δ = 1 : 1 → 1 , . . . , → . We provide a context on Δ ⊢ that translate function calls into a reference write followed by a reference read. We can without loss of generality suppose that all base types involved are int. By assumption, we have that [ ] ≈ ML [ ], which in turn implies that [ ] ≈ [ ] . But it is easy to see that this implies that ≈ : each write to corresponds to a call to with the corresponding argument, and each read to correspond to the return value. We conclude by full abstraction.