# Operational Game Semantics for Generative Algebraic Effects and Handlers

Hamza Jaafar, Guilhem Jaber

► To cite this version:

Hamza Jaafar, Guilhem Jaber. Operational Game Semantics for Generative Algebraic Effects and Handlers. PPDP 2025 - 27th International Symposium on Principles and Practice of Declarative Programming, Sep 2025, Rende, Italy. pp.1-21, 10.1145/3756907.3756924. hal-05166091

HAL Id: hal-05166091

https://hal.science/hal-05166091v1

Submitted on 17 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Operational Game Semantics for Generative Algebraic Effects and Handlers

Hamza Jaafar

Nantes Université

Nantes, France

Guilhem Jaber

Inria / Nantes Université

Nantes, France

## ABSTRACT

We present a sound operational game semantics model (w.r.t. contextual equivalence) of a typed language with algebraic effects and handlers and dynamic generation of effect instances à la [5, 11]. We exhibit the interactive aspect of effect propagation, and to address it precisely, we identify the adequate granularity of the operational semantics (akin to [15]) and the decomposition of normal forms into their interactive and their observational part. To account for this additional form of interaction, we extend the standard pure interaction interface of game semantics consisting of questions and answers with effectful moves that involve the propagation of effects and the yielding of delimited continuations. Finally, we extend the well-bracketed constraint on the behavior of the environment, from the use of continuations as is standard in game semantics, to fragments of captured delimited continuations.

## CCS CONCEPTS

* Theory of computation → Denotational semantics; Control primitives; Operational semantics.

## KEYWORDS

Algebraic Effects, Handlers, Game Semantics

**ACM Reference Format:**

Hamza Jaafar and Guilhem Jaber. 2025. Operational Game Semantics for Generative Algebraic Effects and Handlers. In *Proceedings of The 27th International Symposium on Principles and Practice of Declarative Programming (PPDP'25)*. ACM, New York, NY, USA, 21 pages. https://doi.org/XXXXXXX. XXXXXXX

## 1 INTRODUCTION

Algebraic effects were originally introduced by Power and Plotkin [31, 32] to provide a direct denotational account for syntactic entities that perform effects such as get, set for global state, raise for exceptions, or choose for non-deterministic choice, etc.

The combination of algebraic operations with effect handlers [33] is a more recent and powerful abstraction for programming with effects. Effect handlers generalize exception handlers by giving access not only to the raised effect but also to its delimited continuation. This enables a modular and compositional approach to effectful

programming, supports user-defined effects, and facilitates effect combination in a seamless way.

A central challenge with this abstraction lies in managing multiple occurrences of the same effect while preserving modularity. Two main approaches have been proposed: the lexical approach and the generative approach, as described in [11]. In the lexical approach [8, 9, 34], one introduces effect instances locally, and the handler responsible for these instances is determined statically, preventing instance leakage. This static discipline enforces a form of effect safety, ensuring that all performed effects are handled. In contrast, the generative approach provides the possibility of generating dynamically fresh instances of an effect [5], that can be referred by their names, and be passed around as values. While this increases flexibility, it introduces challenges such as aliasing between names of effect instances, that needs to be tamed in order to enforce effect safety via a type-and-effect-system [11].

In this paper, we adopt the generative approach, but allow for unsafe interaction: effect instances may remain unhandled, and aliasing is not prevented. Our goal is to model the interaction between a program and its environment in such a language. Trace models for higher-order languages capture program behavior as sequences of observable actions -calls and returns- where the arguments of these actions may themselves be (abstractions of) functions. We follow the methodology of operational game semantics (OGS) to define such a trace model.

The central idea of OGS is to represent programs as labelled transition systems (LTS), derived from the operational semantics of the language, in combination with a decomposition of normal forms into observable and interacting parts. This approach is particularly well suited to languages with generative effects, as demonstrated by Laird's seminal work on ML-style higher-order references [22]. OGS also naturally accommodates control operators such as call/cc or the µ-binder capturing the surrounding context of the λµ-calculus [18]. In the absence of such control features, it enforces a well-bracketing discipline on the interaction-matching calls with returns-as is standard in game semantics [2, 17].

To extend OGS to a language with algebraic effect handlers, we incorporate:

* actions representing the execution of an effect;

* a fine-grained representation of the control flow between the program and its environment, to account for the exchange of delimited continuations triggered by handled effects.

Our long-term objective is to obtain a fully abstract trace model, capturing contextual equivalence of our language. As a first step in this direction, we prove that trace equivalence of our model is sound with respect to contextual equivalence. Moreover, we show that a well-bracketing condition can be imposed on the environment's

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

PPDP'25, September 10-11, 2025, University of Calabria, Rende, Italy

© 2025 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM ISBN 978-x-xxxx-xxxx-x/YY/MM

https://doi.org/XXXXXXX.XXXXXXX
interaction. The fact that enforcing well-bracketing does not en-
danger soundness might seem surprising. Indeed, control operators
like call/cc capture the entire undelimited continuation of a com-
putation, breaking well-bracketing by allowing non-local jumps.
But delimited continuation operators—such as those used with al-
gebraic effect handlers—capture only a portion of the continuation
up to a delimiter, so that a relaxed notion of well-bracketing still
holds, enforcing a stack discipline for such delimited continuation.

In the last part of the paper, we exhibit counterexamples to full
abstraction: trace equivalence turns out to be too discriminating to
characterize contextual equivalence.

To keep the model simple, we forbid the exchange of effect in-
stances between the program and its environment. This avoids the
need to dynamically track which effect instances have been dis-
closed—information that would otherwise be required for reasoning
about interactions.

## 2 THE LANGUAGE $\Lambda_{\text{eff}}$

We consider a fine-grained call-by-value programming language [26] with typed algebraic effects and handlers. The language is augmented with dynamical generation of effect instances, in the style of *Eff* [5] We stress that these instances are first-class values that can be exchanged in the same way exceptions or ML-style references, in say OCaml, could be shared. The *generative approach* coupled with the ability to exchange names introduces several challenges to the design of a strong static typing system that rules out unhandled performed effects [11]. We will not address any of these difficulties in the present work.

### 2.0.1 codata and names
We will call *data* all values of positive types that can be fully observed. In contrast, we will call *codata* any $\Lambda_{\text{eff}}$-expression that cannot be fully observed but can only be probed to extract partial observable information (*data*). These include *function-like* expressions: $\lambda$-abstractions and evaluation stacks, as well as *effectful* expressions: much like $\lambda$-abstractions, they can only be inspected by being put in a suitable computation context (a handler) that will trigger evaluation and potentially produce *data*.

Operational methods for proving equivalence of programs typically rely on syntactic tokens in order to observe and collect information about the behaviour of the environment. In the interactive setting of OGS, this is done through names which are semantic artefacts introduced to abstract the codata disclosed by the environment. These names are to be understood as nominal free variables.

In the presence of algebraic effects and handlers, a program not only gets to call functions of the environment, but it can also capture and use fragments of an environment evaluation stack. As it had already been observed in [7], whereas $\lambda$-abstractions belonging to the environment are just free variables, the language provides no syntactic equivalent for the environment's evaluation contexts, therefore it has to be extended to account for them.

In the following, we will consider from the start a language in which these semantic names have been reified as values, evaluation contexts or computations in the syntax. Further details about their role and the process by which they are generated will be however postponed to section 3.1.

## Syntax of types and expressions

We present a nominal syntax that will prove to be expedient to the interactive semantics we are considering in the present paper. This introduces names that are to be understood as generalized variables. They are drawn from a countable set of names $N = \mathcal{L} \cup C \cup \mathcal{K}$ whose names we will range over with $\alpha$. This set is partitioned into function names $\mathcal{L}$ whose elements we range over by $f, g, \text{delimited}$ and undelimited continuation names range over by $\kappa, \chi \in \mathcal{K}$ and $c, d \in C$ respectively, as well as effect names $e \in \mathcal{E}$.

Apart from these names that we highlight in the following fig-
ures, the rest of syntax $\Lambda_{\text{eff}}$ should be standard. We give in figure 1
the algebra of types and the syntax of expressions.

The types are generated from the ground positive types 1, B and N, for unit, booleans and integers respectively, as well as effect types E. The latter are given by their corresponding signatures $\{(\mathbf{op}_i : \tau_i \rightarrow \varphi_i)_{i \in I}\}$ that associate each operation symbol op in the theory of E with its arity $\tau \rightarrow \varphi$, where $\tau$ is the type of its parameter and $\varphi$ is its "return" type, i.e. the type expected by its enclosing continuation. The double-headed arrow $\rightarrow$ distinguishes them from $\lambda$-abstractions.

Application is of the form vw, restricted to values. More general form of application tu between terms can be defined as let x = t in let y = u in xy, specifying explicitly the order of execution, as found in Administrative Normal Form (ANF) languages [13].

The construct new E is responsible for generating a fresh instance of the effect E, whereas the expression l#op v is responsible for performing the effect. It is formed by an operation symbol op associated to an effect E and a particular instance l of this effect, together with a value v that is provided to this operation.

The construct {$t$} with h is responsible for handling these ef-
fects, and it is formed by a potentially effectful term t and a handler
h. The handlers are defined as a non-empty set of clauses; one re-
turn clause of the shape {$\mathit{ret} x \mapsto t$} defining the default behaviour
in case no effect is caught, and a finite set of operation clauses
{$\mathit{l}\#\mathbf{op} x k \mapsto t$} defining the intended behaviour of each operation
symbol op involved.

Given a handler h = {$\mathit{ret} x \mapsto t$} $\circled{\scriptstyle i \in I}$ ($\{i_i \# \mathbf{op}_i x_i k_i \mapsto u_i\}_{i}$), we define h$^\mathrm{ret}$ := {$\mathit{ret} x \mapsto t$} and h$^\mathrm{l}$$_{i}$$_{\#}$$_{\mathbf{op}}_i := \{i_i \# \mathbf{op}_i x_i k_i \mapsto u_i\}$, and hdl(h) := {$\{i_i \# \mathbf{op}_i\}_{i \in I}$} (i.e. the exact set of effects handled by h).

We overload the symbol hdl to define the function that associates an evaluation context to the set of effects it handles.

$$
\begin{align*}
\mathbf{hdl}([\mathbf{t}]) &:= \emptyset & \mathbf{hdl}(\text{let } x = E \text{ in } t) &:= \mathbf{hdl}(E) \\
\mathbf{hdl}(\{E\} \text{ with } h) &:= \mathbf{hdl}(E) \cup \mathbf{hdl}(h)
\end{align*}
$$

$\Lambda_{\text{eff}}$ is also equipped with the standard construct **match** v with p to destruct positive values. Pairs are destructed by being matched with the pattern $\langle x, y \rangle$ of a pattern case of the form $\{\langle x, y \rangle \Rightarrow t\}$, and integers are pattern-matched over using $\{n_0 \Rightarrow t_0, \dots, n_k \Rightarrow t_k\} \uplus \{x \Rightarrow t\}$, where the last pattern serves as a catch-all case for exhaustiveness.

Evaluation contexts S, as introduced in [12], are terms with a
single hole [] that appear in specific positions corresponding to
where the evaluation of a redex may happen, respectively let x= []
in t and [] with h. Their syntax is extended with two notions of
continuation names c and κ, that are a form of free variables used
to represent respectively undelimited and delimited continuations.
Such continuation names are called covariable in the λμ-calculus.
The fact that application is restricted to ANF avoids considering
[] t and v [] as evaluation contexts. Plugging a term inside an
undelimited continuation name c[t] can be understood as a named
term in the λμ-calculus.

We write S[T] for the hole filling operation, that corresponds to
the operation of stacking-up T on top of S.

<figure><img src="image_2.png" /><figcaption>Figure 1: Λ<sub>eff</sub> syntax.</figcaption></figure>

2.1 Typing rules

The full typing system of Λ<sub>eff</sub> is given in figure 2.

We consider two judgement relations ⊢<sub>v</sub> and ⊢<sub>c</sub> defined on values
and terms respectively. The typing contexts are of the shape I; Γ; Θ
where I is an *effect instance context* mapping fresh effect instances i
with their types and where Θ and Γ are typing contexts respectively
for variables and names.

We will often abuse the notations of maps and sets, e.g. Θ(x) or
Γ(α), to denote the type τ such that x : τ ∈ Θ or α : τ ∈ Γ.

The handlers occur in expressions, but are not first-class values.
They are assigned types written τ ⇒ φ (that do not appear in the
grammar of types in figure 1) as well as a distinct typing judgement
given by the relation ⊢<sub>h</sub>. The understanding conveyed is that putting
a computation of type τ inside a handler of type τ ⇒ φ gives a term
of type φ. Again, the double arrow ⇒ distinguishes handlers from
λ-abstractions whose input are values instead of computations.
The rule HANDLER ensures that all the branches of the handler
expect the same type τ and continue computing with the same type
φ guaranteeing a static typing discipline.

The possibility of handling a freshly generated effect instance is
a consequence of the ability to write a handler parametrized by a
variable that can be substituted by this fresh instance, e.g.

let (x)= new B in {t} with {ret y ↦→ t; (x)#op y k ↦→ u}

The rule EFF checks whether the variable has already been instan-
tiated, in which case the corresponding value and its type is to be
found in the context I, otherwise its type is to be found in Θ (like
any other variable in the scope).

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

(b) typing of evaluation contexts.

<caption>Figure 2: type system of Λ<sub>eff</sub></caption>
The type ? denotes the abstract type of some effect name *e*, representing an algebraic effect being performed by the environment, but whose type is *unknown*. Its type is unknown as the enclosing delimited continuation belongs to the environment and could be expecting any type as input.

The typing of evaluation contexts is given by the typing relation $\vdash_S$ which assigns them types of the shape $\tau \rightsquigarrow \varphi$, with the understanding that the following rule is admissible.

$$ \frac{I; \Theta \vdash_S S : \tau \rightsquigarrow \varphi \quad I; \Theta \vdash_c t : \tau}{I; \Theta \vdash_c S[t] : \varphi} $$

When typing undelimited continuation names, we will sometimes use the syntactic sugar $\neg \tau$ for the type $\tau \rightsquigarrow \perp$.

## 2.2 Operational semantics

The propagation of effects through continuation names is to be seen as a form of interaction (in a *game semantics* sense) whereby the *program* inquires whether the *environment’s* code (corresponding to the abstract continuation) handles some specific effect or not. For this reason, we emphasize the stack structure of evaluation contexts and we privilege an abstract machine presentation of the *operational semantics* (à la [15]) whose reduction rules make this flow of information explicit.

The main component of the abstract machine configurations are *running computations* M whose shape is given by:

$$ M := \langle t \mid S \circ T \rangle $$

It consists of the *active term*, *t*, the *forwarded evaluation context*, *T*, followed by the *active evaluation context* *S*, and corresponds to a fine decomposition of the term $S[T[t]]$.

The *reduction relation* $\mapsto_{\text{op}}$ is defined in figure 3 over pairs (M, I) formed by a running computation M and an effect instance context I crucial to provide a semantics to new $\mathbb{E}$. In the following, we will write $\langle t \mid S \circ T \mid I \rangle$ for $(\langle t \mid S \circ T \rangle \mid I)$ and we will often use $\langle t \mid S \rangle$ as *syntactic sugar* for $\langle t \mid S \circ \llbracket \rangle$ and conflate a term *t* with $\langle t \mid \llbracket \rangle$, i.e. its initial embedding in running computations.

The $\mapsto_{\text{push}}$ reduction takes care of the administrative task of unpiling the evaluation frames in the active term in order to expose the underlying redex for $\mapsto_{\text{eval}}$ and $\mapsto_{\text{fwd}}$.

The only non-standard rules are the starred ones ($\star_1$) and ($\star_2$), owing to the presence of names in the syntax.

The rule ($\star_1$) extends the definition of the relation $\mapsto_{\text{fwd}}$ to account for the propagation of effects in the presence of effect names and does that by mirroring the similar preceding rule. Naturally, given that *e* is abstract then so is the underlying effect instance, therefore the top evaluation frame *E* in the active evaluation context cannot *a priori* handle it and should be moved to the forwarded evaluation context. Similarly, the rule ($\star_2$) accounts for continuation names *κ* and *c* when unpiling evaluation contexts.

Notice that we did not add the unsound rule ($\square$) which may seem like the innocuous dual to ($\star_1$).

$$ \langle i \# op v \mid S[\kappa \llbracket] \circ T \rangle \mapsto_{\text{fwd}} \langle i \# op v \mid S \circ \kappa[T] \rangle \quad (\square) $$

Indeed, as it will be evident in section 3, the ability to capture delimited continuations means that the environment can capture fragments of the program’s evaluation context, and as a result, gain control of a program’s handler. Therefore, the possibility of

$$ \langle (\lambda x.t) v \mid S \mid I \rangle \mapsto_{\text{eval}} \langle t \{x := v\} \mid S \mid I \rangle $$

$$ \langle \mathit{match} \langle v, w \rangle \mathit{with} \langle x, y \rangle \Rightarrow t \mid S \mid I \rangle $$

$$ \mapsto_{\text{eval}} $$

$$ \langle t \{x := v\} \{y := w\} \mid S \mid I \rangle $$

$$ \langle \mathit{match} n \mathit{with} p \mid S \mid I \rangle \mapsto_{\text{eval}} \langle t \mid S \mid I \rangle $$

$$ \text{when } \{n \Rightarrow t\} \in p $$

$$ \langle \mathit{match} n \mathit{with} p \mid S \mid I \rangle \mapsto_{\text{eval}} \langle t \{x := n\} \mid S \mid I \rangle $$

$$ \text{when } \{n \Rightarrow \}_ \notin p \wedge \{x \Rightarrow t\} \in p $$

$$ \langle \mathit{new} \mathbb{E} \mid S \mid I \rangle \mapsto_{\text{eval}} \langle \mathit{ret} \iota \mid S \mid I \cdot [\iota \mapsto \mathbb{E}] \rangle $$

$$ \langle \mathit{ret} v \mid S[\mathit{let} x = \llbracket \mathit{in} t \rangle \mid I] \rangle \mapsto_{\text{eval}} \langle t \{x := v\} \mid S \mid I \rangle $$

$$ \langle \mathit{ret} v \mid S[\llbracket \rangle \mathit{with} h] \mid I \rangle \mapsto_{\text{eval}} \langle t \{x := v\} \mid S \mid I \rangle $$

$$ \text{when } h^{\text{ret}} = \{\mathit{ret} x \mapsto t\} $$

$$ \langle i \# op v \mid S[\llbracket \rangle \mathit{with} h] \circ T \mid I \rangle $$

$$ \mapsto_{\text{eval}} $$

$$ \langle t \{x := v\} \{y := \lambda z. \langle T[\mathit{ret} z] \rangle \mid \mathit{with} h \} \mid S \mid I \rangle $$

$$ \text{when } h^{\text{OP}} = \{i \# op x y \mapsto t\} $$

$$ \langle i \# op v \mid S[E] \circ T \mid I \rangle \mapsto_{\text{fwd}} \langle i \# op v \mid S \circ E[T] \mid I \rangle $$

$$ \text{when } i \# op \notin \mathit{hdl}(E) $$

$$ \langle e \mid S[E] \circ T \mid I \rangle \mapsto_{\text{fwd}} \langle e \mid S \circ E[T] \mid I \rangle \quad (\star_1) $$

$$ \langle E[T] \mid S \mid I \rangle \mapsto_{\text{push}} \langle t \mid S[E] \mid I \rangle $$

$$ \langle \alpha[T] \mid S \mid I \rangle \mapsto_{\text{push}} \langle t \mid S[\alpha \llbracket] \mid I \rangle \quad (\star_2) $$

<caption>Figure 3: operational semantics</caption>

$\kappa \llbracket$ handling the effect (even though $i \# op v$ is abstract from the environment's perspective) cannot *a priori* be ruled out.

*Non-termination.* Recursion and divergence can be restored with Landin's knot[24] through an encoding of higher-order state using handlers. We illustrate with the following diverging term, that we will denote by $\Omega$, the shape of the *backpatching* it involves.

$$ \text{let } f = \left( \begin{array}{@{}l@{}} \{\text{let } f = i \# \text{read } \langle \iota \rangle \text{ in } f \} \text{ with} \\ \quad | \text{ret } x \mapsto \text{ret } (\lambda g. \text{ret } x) \\ \quad | i \# \text{read } \langle \iota \rangle k \mapsto \text{ret } (\lambda g. k g) \end{array} \right) \\ \text{in } f (\lambda x. \text{let } y = i \# \text{read } \langle \iota \rangle \text{ in } y x) $$

(1) $\Omega$ encodes a higher-order state reader effect given by the signature $\{\text{read} : \mathbb{I} \to (\mathbb{1} \to \mathbb{1})\}$ with the handler $^1 h = \{\text{ret } x \mapsto \text{ret } (\lambda g. \text{ret } x); i \# \text{read } \langle \iota \rangle k \mapsto \text{ret } (\lambda g. k g)\}$ reading from a "cell" identified by the effect instance $i$.

(2) The state is initialised with $\lambda x. \text{let } y = i \# \text{read } \langle \iota \rangle \text{ in } y x$, which reads a function from the "cell" $i$, binds it to $y$ and then passes its argument to it.

<footnote>$^1 k g$ is syntactic sugar for $\text{let } x = k g$ in $x g$.</footnote>
(3) The term $\mathit{let} f = i \# \mathit{read} \langle \rangle \mathit{in} f \langle \rangle$ makes a call to this un-
guarded self-calling function and triggers the loop.

Notations: We will write (M | I) ↦ x, where x ∈ {op, eval, fwd}
to indicate that there exist an effect instance context I' and a term
N such that (M | I) ↦ x (N | I'). Its negation will be denoted by
(M | I) ↦ x.

We will also write (M | I) ⇝op (N | I') to mean that (M | I) ↦*op
(N | I') and that (N | I') ↦>op, and the notation (M | I) ⇝op will be
used to assert the existence of I' and N in s.t. (M | I) ⇝op (N | I').

For divergence, we will adopt the notation (M | I) ⇝op to indicate
that (M | I) diverges, i.e. for all (N | I') such that (M | I) ↦*op
(N | I') then (N | I') ↦>op.

2.3 Metatheory

2.3.1 *Interactive/Private fragment.* In the following, we will mostly be interested in the *interactive* and *private* subset of terms and computations on which our OGS semantics operate. In this fragment, generated instances remain private to the program and are never made available to the external environment.

Since the syntax of expressions of such a fragment does not
differ from that Λ<sub>eff</sub>, we will capture it by a restricted typing judge-
ment relation ⊢<sub>c</sub> ⊂ ⊢<sub>c</sub>, that will ensure that no effect instances can
be exchanged between the program and its environment. Indeed,
given an Λ<sub>eff</sub>-term I; Θ ⊢<sub>c</sub> t : τ, the possibility of t exchanging
effect instances with a compatible environment is indicated by the
occurrence of effect signatures E in Γ.

*Definition 2.1 (interactive expressions).* A term *t* is said to be *interactive* when it is well-typed and admits a typing of the form
*I*; Γ ⊢<sub>*c*</sub> *t*, defined as

$$
\frac{I; \Gamma; \emptyset \vdash_c t : \perp \qquad \text{codom}(\Gamma) \subset \mathcal{P}}{I; \Gamma \vdash_c t}
$$

where $\mathcal{P}$ is the smallest set of types that subsumes $\{\mathbf{1}, \mathbf{B}, \mathbf{N}\}$ and
is closed by the type constructors $\rightarrow$, $\rightleftharpoons$, $\times$ and $\neg$.

A running computation M is said to be *interactive* and written
$I; \Gamma \vdash_c M$ when the underlying term is interactive, i.e.

$$
\frac{I; \Gamma; \emptyset \vdash_c S[\Gamma[t]] : \perp}{I; \Gamma \vdash_c \langle t | S \circ T \rangle}
$$

2.3.2 Normal forms. Since normal forms describe the interaction
interface between the program and its environment, we will privi-
lege a useful presentation where we identify the interaction patterns
that are causing a computation to be stuck. By explicitng these
patterns, the normal forms are written as P(α); they involve a copat-
tern P (described in figure 5) representing the program controlled
code and a name α abstracting an environment controlled codata.
The token □ represents a codata hole whose filling, i.e. the syntactic
substitution thereof, is given by the application (P, x) ↦ P(x) of
copatterns to codata defined as P(x) := P{□ ↦ x}.

Borrowing from the terminology of [7], we identify in figure 4
open-stuck terms in which the reduction of the term depends on an
abstract function f or an abstract delimited continuation κ[] and
where the continuation is controlled by the program, as well as
context-stuck terms corresponding to unhandled effects and fully-
evaluated returners inside an abstract continuation c[].

Borrowing from the terminology of [7], we identify in figure 4
open-stuck terms in which the reduction of the term depends on an
abstract function *f* or an abstract delimited continuation *κ[]* and
where the continuation is controlled by the program, as well as
context-stuck terms corresponding to unhandled effects and fully-
evaluated returners inside an abstract continuation *c[]*. The two

Nf ::= (ret v | c[] ) | (ret v | S[κ[]]) evaluated returners
| (e | S[κ[]] ◦ T) | (e | c[] ◦ T) unhandled effects
| (f v | S) open applications

<caption>Figure 4: interactive normal forms of Λ<sub>eff</sub>.</caption>

classes of normal forms correspond to different forms of interaction;
the former calls for a *question* whereas the latter for an *answer*.

P ::= <ret v | □> |<e | □ ◦ S>
    | <ret v | S[□]> |<e | S[□] ◦ T>
    | <□ v | S>

context-stuck
open-stuck

(a) syntax of copatterns

$$
\left.
\begin{array}{l}
\text{CONT-VAL} \\
\frac{I; \Gamma \vdash_v v : \tau}{I; \Gamma \vdash_p \langle \text{ret } v \mid \Box \rangle : \neg\neg\tau}
\end{array}
\right\}
\quad \text{context-stuck}
$$

$$
\left.
\begin{array}{l}
\text{LAMBDA} \\
\frac{I; \Gamma \vdash_v v : \tau}{I; \Gamma \vdash_p \langle \Box v \mid S \rangle : \neg(\tau \to \varphi)}
\end{array}
\right\}
\quad \text{open-stuck}
$$

(b) typing judgements for copatterns

<caption>Figure 5: copatterns: syntax and types.</caption>

The interactive fragment of Λ<sub>eff</sub> satisfies the two following prop-
erties pertaining to type preservation and normal forms.

LEMMA 2.2 (SUBJECT REDUCTION). *Given two interactive running computations M and N s.t. I; Γ ⊢<sub>c</sub> M and (M | I) ↦>op (N | I'), then I'; Γ ⊢<sub>c</sub> N.*

LEMMA 2.3 (NORMAL FORMS SHAPE). For all interactive computa-
tions I; Γ ⊢<sub>c</sub> M such that (M | I) ↦>op, there exists a copattern P and
a name α ∈ dom(Γ) s.t. M = P(α).

Our notion of program equivalence builds on the Closed Instan-
tiations of Uses (CIU) equivalence, introduced by Mason and Tal-
cott [27]. Whereas Morris-style contextual equivalence [28] quan-
tifies over general contexts—including those placing holes under
λ-abstractions to handle open terms—CIU-equivalence restricts
attention to evaluation contexts and handles open terms by quanti-
fying over substitution maps as well.

In our setting, we refine this idea by leveraging the distinction
between variables and names: we define equivalence only for in-
teractive terms I; Γ ⊢<sub>c</sub> M, where M contains no free variables, and
all names are drawn from $\Gamma$. We assume that $\Gamma$ contains exactly one continuation name, and no delimited continuation names. We refer to such typing contexts as initial, since these constraints do not generally hold as interaction proceeds. Equivalence between $M_1$ and $M_2$ is then defined via mutual approximation. Quantifying over all name assignments for $\Gamma$, the continuation name $d$ is interpreted as an evaluation context. This yields a form of CIU-equivalence based solely on quantification over name assignments.

We start by introducing the type judgements for name assignments that we range over by $\gamma$, $\delta$.

$$I; \Gamma \vdash \gamma : \Delta := \forall \alpha \in \text{dom}(\gamma). \exists x \in \{v, c, s\}. I; \Gamma \vdash_X \gamma(\alpha) : \Delta(\alpha)$$

We will use $\varepsilon$ to denote an empty name assignments (map).

**Definition 2.4 (ciu-approximation).** We consider two interactive terms $M_1, M_2$ such that both $\emptyset$; $\Gamma \vdash_c M_i$ (for $i \in \{1, 2\}$), with $\Gamma$ initial. Then $M_1$ is said to be *ciu-approximated* by $M_2$, written $\Gamma \vdash M_1 \leq_{ciu} M_2$, when for all instance contexts $I$, for all continuation names $c_f$ and for all name assignments $\gamma$ such that $I; c_f : \neg I \vdash \gamma : \Gamma$, if $(M_1\{\gamma\} | I) \Downarrow_{op} c_f[\langle\rangle]$ then $(M_2\{\gamma\} | I) \Downarrow_{op} c_f[\langle\rangle]$.

We note that this definition excludes terms with names of positive types such as $\mathbb{B}$ or $\mathbb{N}$, which should rather be handled using free variables. A mild generalization of our approach could accommodate such terms by also quantifying over variable substitutions. However, for the sake of simplicity, we leave this extension to future work.

# 3 REPRESENTING INTERACTION

In this section, we describe the *interactive execution* of a term (*Propponent*) with an abstract *environment* (*Opponent*) through a bipartite labelled transition system $\mathcal{L}_{OGS}$. This is achieved in §3.5 by synchronizing the interaction LTS $\mathcal{L}_{AI}$ with two disciplinary LTSs $\mathcal{L}_T$ and $\mathcal{L}_{wb}$ that constrain Opponent's behaviour to conform to what is possible for an environment written in $\Lambda_{eff}$ as well. These LTSs are introduced as follows:

* In §3.1, we introduce the key decomposition process of a normal form of $\Lambda_{eff}$ into their observable part and their interacting part.

* In §3.2, we define $\mathcal{L}_{AI}$ that characterizes the general game of interaction of $\Lambda_{eff}$, based on this decomposition of normal forms.

* In §3.3, we define $\mathcal{L}_T$ that characterizes the type discipline of the interaction inherent to the typing of $\Lambda_{eff}$.

* In §3.4, the well-bracketing condition constraining the way delimited continuations can be used in $\Lambda_{eff}$ is characterized by $\mathcal{L}_{wb}$.

## 3.1 Nominal abstraction

When an *active term* reaches a *normal form*, it discloses only the information needed (i.e. at the appropriate level of *abstraction*) for the environment to continue computing a value.

In a dual manner, upon receiving a this information, the *passive environment* (who knows its type) inspects its structure to infer the types of the underlying abstract components.

This is achieved through an *abstraction* and an appropriate *type inference* processes.

**abstraction process:** It is essentially the process that transforms a *syntactic object* into an ultimate pattern [25] (its positive skeleton) together with a corresponding name assignment map (its negative filling). Therefore given an object $o$, it generates a *nominal pattern* $p$ and a name assignment $\gamma$ with the understanding that $o = p\{\gamma\}$. Concretely, the codata occurring in the syntactic object are abstracted away and transformed into *names* to be handed over to the environment as part of various *nominal patterns*, capturing the fact that the latter's behaviour can only be parametric w.r.t. these *codata* (unlike *data* that could be inspected to trigger a *data-dependent reaction*).

**nominal type inference:** The general form of judgements in the type inference systems is the following: $\Gamma \vdash p : \tau \triangleright \Delta$; that is given a nominal pattern $p$ of some expected type $\tau$ (inputs), this process infers the type of every name $n \in \text{supp}(p)$ occurring in $p$ and returns a name type context $\Delta$ (ouptput).

In the following, we will define the *nominal abstraction* of a few syntactic categories, where we will first introduce, for each, their abstract counterpart.

**3.1.1 Abstract values.** These are the values exchanged between Proponent and Opponent during their interaction. They are defined over a set of *function names* $f \in \mathcal{L}$:

$$V, W := \langle\rangle | n | \mathfrak{f} | \mathfrak{t} | f | \langle V, W \rangle$$

We define in figure 6 the corresponding abstraction process of values, denoted by the infix symbol $\frown$, and the type inference system.

<figure><img src="image_4.png" /><figcaption>(b) abstraction of generalised values.</figcaption></figure>

<caption>Figure 6: nominal abstraction process.</caption>

**3.1.2 Abstract generalised values.** Not only the structure of values is exposed in the interaction of Opponent and Proponent, but so are
some fully-evaluated computations. These generalised values<fnref n="2" /> are
in turn abstracted away into patterns; nominal generalised values,
which are defined as:

$$
C, D := \mathbf{ret} \mathbf{V} | e | r[e]
$$

where $e \in \mathcal{E}$ is an abstract *effect name* and $r \in \text{List}(\mathcal{K})$ is a *abstract*
*(delimited) evaluation stack* defined over the set $\mathcal{K}$ of *delimited*
*continuations names*.

Analogously to abstract values, we define the nominal abstrac-
tion of generalised values in figure 6, where the abstraction process
is denoted by ⏟.

The type inference judgements are written Γ ⊢ C : τ ⊢ Δ₁; Δ₂
where the inferred type context is split into two: the first one for
function names and the second one for effect and delimited contin-
uation names.

3.1.3 Abstract normal forms. Continuing with our nominal abstrac-
tion of expressions, we introduce abstract normal forms and abstract
copatterns and for the sake of a uniform treatment in-keeping with
the classification of copatterns of figure 5, we will express them in
terms of abstract computations in order to exhibit the underlying
generalized questions and answers structure.

$$
\begin{array}{l@{\hspace{1em}}c@{\hspace{1em}}l}
p, q & ::= & \langle C \mid \Box \rangle \\
      &   | & \langle \Box C \mid d \rangle | \langle \Box V \mid d \rangle
\end{array}
\qquad
\begin{array}{l}
\text{context-stuck} \\
\text{open-stuck}
\end{array}
$$

where $\langle r[e] | \Box \rangle$, $\langle \Box [r[e]] | d \rangle$ and $\langle \Box [\mathbf{ret}V] | d \rangle$ are syntactic
sugar for $\langle e | \Box \circ r \rangle$, $\langle e | d[\Box] \circ r \rangle$ and $\langle \mathbf{ret}V | d[\Box] \rangle$ respectively,
and where the hole filling is given by the application $(p, \alpha) \mapsto p[\alpha]$
where $p[\alpha] := p\{\Box := \alpha\}$.

In figure 7 we introduce the nominal abstraction of copatterns.
Naturally, the abstraction process produces an abstract copattern,
a name assignment $\gamma$, in addition to a component $\xi$, the abstract
forward, carrying information about the forward evaluation stack.
It is either of the shape $\emptyset$ (indicating the absence of effects) or
$(e, r, \delta)$ (indicating a performed effect $e$ to be forwarded or handled)
where $r$ represents the abstract (delimited) stack through which said
effect has been propagated and $\delta$ is another name assignment for
abstracting the effects and the surrounding evaluation contexts.

The type inference system similar to the one for generalised
values in that it maintains two distinct name type contexts Γ and Δ
where the first one contains function and undelimited continuation
names, whereas the second one is only for effect and delimited
continuation names.

Note that in this definition we use abstract evaluation contexts
F that are either a stack of evaluation frames E or just a hole [].
The former case reflects the fact that only the concrete fragments
of the evaluation contexts are abstracted, wheras the latter case
reflects the fact that the abstraction of both E[i#opv] and i#opv
should result in a pattern of the form κ[e] where κ represents
either E or []. Indeed, omitting κ when abstracting i#opv breaks
the uniformity and carries an information (that the surrounding
delimited continuation is the identity) that should not be disclosed.

*Example 3.1.* Perhaps the simplest example is a fully-evaluated
returner in the form of c[ret v] that can be written as (□ ret v)(c)
and whose abstraction can be expressed as an abstract copattern
$p = \langle \mathbf{ret} \mathbf{V} | \Box \rangle$ and the abstract codata c.

$$
\frac{\text{CONTEXT-STUCK} \quad \begin{array}{@{}c@{}} \vcenter{\hbox{\texttt{v \nearrow (V, \gamma_V)}}} \\ \langle \text{ret} \mathbf{v} | \Box \rangle \nearrow \langle (\text{ret} \mathbf{v} | \Box), \gamma_V, \emptyset \rangle \end{array}}{\text{RETURN}}
$$

PERFORM

$$
\langle i \# \mathbf{op} v | \Box \circ F \rangle \nearrow \langle (\kappa[e] | \Box), \epsilon, (e, \kappa, [e \mapsto i \# \mathbf{op} v] \cdot [\kappa \mapsto F]) \rangle
$$

FORWARD

$$
\langle e | \Box \circ F[r] \rangle \nearrow \langle (\kappa \circled{=} r[e] | \Box), \epsilon, (e, \kappa \circled{=} r, [\kappa \mapsto F]) \rangle
$$

where $F ::= [] | F[E]$

OPEN-STUCK

$$
\frac{\mathbf{v} \nearrow (\mathbf{V}, \mathbf{\gamma}_\mathbf{V})}{\langle \Box \mathbf{v} | \mathbf{S} \rangle \nearrow \langle (\Box \mathbf{v} | \mathbf{c}), \gamma_\mathbf{V} \cdot [\mathbf{c} \mapsto \mathbf{S}], \emptyset \rangle}
$$

$$
\frac{\mathbf{P} \nearrow (\mathbf{p}, \mathbf{\gamma}, \mathbf{\xi})}{\mathbf{C}[\mathbf{S}[\Box]] \nearrow (\mathbf{p}[\mathbf{c}[\Box]]), \mathbf{\gamma} \cdot [\mathbf{c} \mapsto \mathbf{S}], \mathbf{\xi}]
$$

(a) abstracting copatterns

$$
\frac{\text{CONTEXT-STUCK} \quad \begin{array}{@{}c@{}} \Gamma \vdash_C C : \tau \vdash \Gamma_C; \Delta_C \\ \Gamma \vdash_P \langle C | \Box \rangle : \neg \neg \tau \vdash \Gamma_C; \Delta_C \end{array}}{\quad}
$$

$$
\frac{\text{OPEN-STUCK} \quad \begin{array}{@{}c@{}} \Gamma \vdash_C C : \tau \vdash \Gamma_C; \Delta_C \\ \Gamma \vdash_P \langle \Box C | d \rangle : \neg (\tau \leadsto \varphi) \vdash \Gamma_C, d : \neg \varphi; \Delta_C \end{array}}{\quad}
$$

$$
\frac{\vdash_V V : \tau \vdash \Gamma_V}{\Gamma \vdash_P \langle \Box V | d \rangle : \neg (\tau \to \varphi) \vdash \Gamma_V, d : \neg \varphi; \emptyset}
$$

(b) copatterns typing rules.

<caption>Figure 7: nominal abstraction of copatterns.</caption>

REMARK 1. Notice how the abstraction process of normal forms is not total. It is only defined on effectful normal forms of a specific shape (involving the evaluation contexts F) that reflects the order of effect propagation and the incrementation of the abstract forward mirrors this gradual interactive process. The choice of keeping $\gamma$ and $\delta$ (of $\xi$) and to combine abstract codata belonging to both the program and the environment in $r$ has a technical benefit as well as a conceptual one; as it maintains the distinction between passive interactions and interactions with observation.

3.2 Interaction LTS

In the *abstract interaction*, the executing term (Proponent) will be
represented by an LTS configuration in order to be evaluated against
an *abstract environment* (Opponent) that models all compatible
*program environments* while exhibiting the *interaction* between
the two that gets obscured by plain *syntax substitution*. To this
effect, the configurations will carry an *information* component that
keeps track of the history of the *interaction*. It consists of a map
between the names and the *concrete* code of codata that Proponent
has disclosed and rendered accessible to Opponent.

<footnote n="2">²computations that *are* but cannot *do*.</footnote>
We define next the abstract interactive LTS $\mathcal{L}_{AI}$ that is given by $(\mathcal{A}, M, \xrightarrow{m})$.

### 3.2.1 configurations, moves and transitions.

states $\mathcal{A} \ni I, J ::= \langle I; \gamma; \Box \xi \rangle$ passive state
$| \langle (M | I); \gamma; \Box \delta \rangle$ active state

moves $M \ni m := \alpha.p^{\oplus} | \alpha.p^{\ominus}$

The moves are given by the previously described abstract copatterns where the action $\alpha.p$ is to be understood as the combination of an interaction handle $\alpha$ and an input $p$: the abstract codata $\alpha$ belonging to the passive player is being probed with the active player's abstract copattern $p$.

Putting a modality $\Box \in \{!, ?\}$ in front of the abstract forward $\xi$ indicates who is the author of the effect. Accordingly, $!, (e, \_\delta)$ means that Proponent performed the effect and that Opponent can only forward it, while $?\delta$, on the other hand, reads as Opponent may forward the effect.

Note that is only a convenient notation since the former case would always be witnessed by the fact that $e \in \text{dom}(\delta)$ and the latter by $\text{dom}(\delta) \cap \mathcal{E} = \emptyset$. For this reason we will often omit writing the modality. We will also omit the abstract forward altogether from configurations when it is equal to $\emptyset$, i.e. $\langle I; \gamma \rangle$ (resp. $\langle (M | I); \gamma \rangle$) is syntactic sugar for $\langle I; \gamma; \emptyset \rangle$ (resp. $\langle (M | I); \gamma; \emptyset \rangle$).

For a compact presentation, we will abuse the notation of maps and substitution on $\xi$ when it is the constituting component $\delta$ that is intended instead.

The superscript $\oplus$ (resp. $\ominus$) is there to indicate that Proponent (resp. Opponent) is the active player performing the move. We will sometimes range over these polarized moves by $p$ and $o$ respectively. Breaking down all the possible interactive transitions witnessed by $\alpha.p$, we have:

c. $\langle \text{ret} \vee | \Box \rangle$ returning a value to the abstract context $c$.

c. $\langle r[e] | \Box \rangle$ propagating $e$ and the delimiting continuation $r$ to the abstract context $c$.

f. $\langle \Box \vee | d \rangle$ requesting the result of the application $f \vee$ in $d$.

κ. $\langle \Box[\text{ret} \vee] | d \rangle$ requesting the result of the computation $\kappa[\text{ret} \vee]$ in $d$.

κ. $\langle \Box[r[e]] | d \rangle$ delegating the handling or propagation of $e$ with its delimiting continuation $r$ to $κ$ and requesting the result in $d$.

After a series of internal reduction steps $\mapsto^{*}_{op}$, the active configuration reaches a normal form. It performs a transition into an passive state where the codata in the corresponding copattern is abstracted then disclosed or forwarded to the environment via the information components. The underlying abstraction process is defined in figure 8, where abstract$(P[\alpha], \xi] \unlhd (\alpha.p, \gamma, \xi')$ is to be read as abstract taking a decomposed normal form and an effect forward component $\xi$ and producing the next action $\alpha.p$ and the corresponding information components $\gamma, \xi'$.

A transition from a passive configuration admits branching. Indeed, since the program environment is abstract and not fixed, it can use any of the disclosed information to perform a move triggering a transition into an active configuration and the concretization of a running computation. This process is given by the function concretize

PURE
$$ \mathbf{P} \unlhd (p, \gamma_p, \emptyset) $$
abstract$(\mathbf{P}[\alpha], \emptyset) \unlhd (\alpha.p, \gamma_p, \emptyset)$

PERFORM
$$ \langle i \# op \vee | S[\Box] \circ F \rangle \unlhd (p, \gamma_p, \xi) $$
abstract$(\langle i \# op \vee | S[\alpha] \rangle \circ F), \emptyset) \unlhd (\alpha.p, \gamma_p, \xi)$

FORWARD
$$ \langle e | S[\Box] \circ F[r] \rangle \unlhd (p, \gamma_p, \xi) $$
abstract$(\langle e | S[\alpha] \rangle \circ F[S]), (e, r, \_\delta) \unlhd (\alpha.p, \gamma_p, \xi)$

(a) abstracting normal forms

PURE/PERFORM
$$ \text{concretize}(\alpha.p, \gamma, \emptyset) = p[\gamma(\alpha)] $$

FORWARD
$$ \xi = (e, r, \delta) \quad p = \langle \kappa \vdash r[e] | \_ \rangle \quad \mathbf{P} = p\{\delta\} $$
$$ \text{concretize}(\alpha.p, \gamma, \xi) = \mathbf{P}[\gamma(\alpha)] $$

(b) concretizing abstract normal forms

<caption>Figure 8: the dualizing process.</caption>

defined in figure 8, which takes as input an action $\alpha.p$, the disclosed information $\gamma$ and $\xi$ in order to output the corresponding running computation shaped $\mathbf{P}[\gamma(\alpha)]$.

The transitions of $\mathcal{L}_{AI}$ are then defined in figure 9.

**REMARK 2.** As mentioned in section 2.2 where we have introduced $\mapsto_{op}$, the reduction $\mapsto_{fwd}$ captures a flow of information; that of effect propagation. A series of $\mapsto_{fwd}$ reductions not followed by an $\mapsto_{eval}$ reduction results in an unhandled effect forwarded to the environment, which in turn could potentially handle it, capturing the associated delimited continuation in the process.

This information flow is a form of interaction between the program and its environment consisting in inquiring whether the environment handles the effect or not. The abstract effect and its enclosing evaluation context are provisionally forwarded as a fragment of the would-be captured delimited continuation in case the environment catches the effect and handles it. In case it does not, a pseudo copy-cat action (forwarding back the same effect but with an extended evaluation context) is expected instead.

By way of example, we will give an informal presentation of the interaction of a term with a concrete program context, which will map to one possible interactive execution path against an abstract environment in $\mathcal{L}_{AI}$.

**Example 3.2.** We consider the interaction of the term $u := \text{let } y = \text{new } \mathbb{B}$ in $\{f(\lambda x.y \# op(\langle \cdot \rangle))\} \text{ with } h^y := \{\text{ret } x \mapsto \text{ret } x\} \cup \{y \# op x \kappa \mapsto \kappa 5\}$, with the program context $\text{let } f = (\lambda y.y \vee; \text{ret } t) \text{ in } []$, that is in turn equivalent to the ciu-environment $([	ext{f} \mapsto \lambda g.g \vee; \text{ret } t])$.

We embed the term $u$ into the active configuration $\langle d_0[u], \varepsilon \rangle$. Moreover, we consider the passive configuration $\langle \gamma_0 \rangle$ representing the ciu-environment, where $\gamma_0 = [d_0 \mapsto c_f[]] \cdot [f \mapsto \lambda x.x \vee; \text{ret } t]$.
$$ \mathbf{EVAL} \frac{(M | I) \mapsto_{\mathbf{eval}} (N | I')}{\langle (M | I); \gamma \rangle \stackrel{\mathbf{eval}}{\longrightarrow} I \langle (N | I'); \gamma \rangle} $$

(a) Internal evaluation

$$ \mathbf{Px} \frac{\mathbf{abstract}(\mathbf{Nf}, \emptyset) \rightleftharpoons (\boldsymbol{\alpha}.\mathbf{p}, \gamma_{\mathbf{p}})}{\langle (\mathbf{Nf} | I); \gamma \rangle \xrightarrow{\boldsymbol{\alpha}.\mathbf{p}^{\oplus}} I \langle I; \gamma \cdot \gamma_{\mathbf{p}} \rangle} $$

$$ \mathbf{Ox} \frac{}{\langle I; \gamma \rangle \xrightarrow{\boldsymbol{\alpha}.\mathbf{p}^{\ominus}} I \langle \langle \mathbf{p}[\gamma(\boldsymbol{\alpha})] | I \rangle; \gamma \rangle} $$

(b) Pure moves

$$ \mathbf{FORWARD} \frac{\mathbb{I} \stackrel{s}{\rightleftharpoons}_{\mathbf{fwd}} \mathbb{J}}{\mathbb{I} \stackrel{s}{\rightleftharpoons}_{I} \mathbb{J}} $$

(c) Effect forwarding sequences

$$ \mathbf{FORWARD} \frac{(M | I) \mapsto_{\mathbf{fwd}} (N | I')}{\langle (M | I); \gamma; \xi \rangle \to_{\mathbf{fwd}} \langle (N | I'); \gamma; \xi \rangle} $$

$$ \mathbf{PHANDLE} \frac{(M | I) \mapsto_{\mathbf{eval}}}{\langle (M | I); \gamma; !\delta \rangle \xrightarrow{\mathit{hdl}^{\oplus}} \mathbf{fwd} \langle (M\{\gamma\} | I); \gamma \rangle} \quad \mathbf{OHANDLE} \\ \langle I; \gamma; ?\xi \rangle \xrightarrow{\mathit{hdl}^{\ominus}} \mathbf{fwd} \langle I; \gamma \cdot \xi \rangle $$

(d) Internal effect manipulation

$$ \mathbf{PEFF} \frac{\mathbf{abstract}(\mathbf{Nf}, \delta) \rightleftharpoons (\boldsymbol{\alpha}.\mathbf{p}, \gamma_{\mathbf{p}}, \xi)}{\langle (\mathbf{Nf} | I); \gamma; \delta \rangle \xrightarrow{\boldsymbol{\alpha}.\mathbf{p}^{\oplus}} \mathbf{fwd} \langle I; \gamma \cdot \gamma_{\mathbf{p}}; \xi \rangle} $$

$$ \frac{\mathbf{concretize}(\boldsymbol{\alpha}.\mathbf{p}, \gamma, \xi) = (M, \delta)}{\langle I; \gamma; \xi \rangle \xrightarrow{\boldsymbol{\alpha}.\mathbf{p}^{\ominus}} \mathbf{fwd} \langle (M | I); \gamma; \delta \rangle} \quad \mathbf{OEFF} $$

(e) Effectful moves

<caption>Figure 9: transitions of the Interaction LTS</caption>

Reading from top to bottom, the figure. 10 illustrates their concrete interaction as well as its corresponding *path* in the *abstract interaction* LTS. After every interaction point, the active player plays a move and swaps roles with the *passive* player. The codata $\alpha$ that underlies the move is highlighted like so $\alpha$.

## 3.3 Typing Constraints

Definition 3.3. Type configurations $\mathbb{T}; \mathbb{S}$ are of the shape $\langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle$ where:

* $\Gamma_p, \Gamma_o$ are two disjoint type contexts for Program names and Environment names, respectively.

$$ d_0, f \quad \mathbf{:=} \quad d_0[\{\mathbb{f}\} (\lambda x.\mathbf{i}\#\mathbf{op}(\langle\rangle)] \text{ with } h'] \\ \frac{}{} \quad f.\langle\square g | c_0\rangle^{\oplus} $$

$$ c_0, g \quad \mathbf{:=} \quad \begin{array}{l} c_0[(\lambda y.y n; \mathbf{ret} \mathbb{t}) g] \\ \mathbf{\downarrow} \mathbf{eval} \\ c_0[\mathbb{g} n; \mathbf{ret} \mathbb{t}] \end{array} $$

$$ d_0, f, d_1 \quad \mathbf{:=} \quad \begin{array}{l} d_1[(\lambda x.\mathbf{i}\#\mathbf{op}(\langle\rangle) n] \\ \mathbf{\downarrow} \mathbf{eval} \\ \boxed{d_1} \mathbf{i}\#\mathbf{op}(\langle\rangle) \end{array} $$

$$ c_0, g! (e, \kappa) \quad \mathbf{:=} \quad \begin{array}{l} c_0[\kappa[e]; \mathbf{ret} \mathbb{t}] \\ \mathbf{\downarrow} \mathbf{fwd} \\ \langle e | \boxed{c_0} \rangle | \kappa[\Box]; \mathbf{ret} \mathbb{t} \rangle \end{array} $$

$$ c_0, g, \kappa \quad \mathbf{:=} \quad \begin{array}{l} c_0[\kappa[e]; \mathbf{ret} \mathbb{t}] \\ \mathbf{\downarrow} \mathbf{fwd} \\ \langle e | \boxed{c_0} \rangle | \kappa[\Box]; \mathbf{ret} \mathbb{t} \rangle \end{array} $$

$$ d_0, f, d_1! (e, \kappa; \kappa) \quad \mathbf{:=} \quad \begin{array}{l} \langle \mathbf{i}\#\mathbf{op}(\langle\rangle) | d_0[\{\Box\}] \text{ with } h' \rangle | \kappa[\Box] \rangle \\ \mathbb{J}_{\mathit{hdl}} \\ \langle (\lambda y.\{\kappa[\mathbf{ret} y]\} \text{ with } h') 5 | d_0[\Box] \rangle \end{array} $$

$$ d_0, f, d_1, [\kappa] \quad \mathbf{:=} \quad \begin{array}{l} \mathbf{\downarrow} \mathbf{eval} \\ \langle \mathbf{ret} 5 | d_0[\{\Box\}] \rangle \text{ with } h' \rangle \end{array} $$

$$ c_0.\langle \square[\mathbf{ret} 5] | c_1 \rangle^{\oplus} \quad \mathbf{:=} \quad \begin{array}{l} \langle \mathbf{ret} 5; \mathbf{ret} \mathbb{t} | c_1 \Box \rangle \\ \mathbf{\downarrow} \mathbf{op} \\ \boxed{c_1}[\mathbf{ret} \mathbb{t}] \end{array} $$

$$ c_0, g, c_1 \quad \mathbf{:=} \quad \begin{array}{l} \mathbf{\downarrow} \mathbf{op} \\ \boxed{c_1}[\mathbf{ret} \mathbb{t}] \end{array} $$

$$ c_1.\langle \mathbf{ret} \mathbb{t} | \square \rangle^{\oplus} \quad \mathbf{:=} \quad \begin{array}{l} d_0[\{\mathbf{ret} \mathbb{t}\} \text{ with } h'] \\ \mathbf{\downarrow} \mathbf{eval} \\ \boxed{d_0}[\mathbf{ret} \mathbb{t}] \end{array} $$

$$ c_0, f, d_1, [\kappa] \quad \mathbf{:=} \quad \begin{array}{l} d_0[\{\mathbf{ret} \mathbb{t}\} \text{ with } h'] \\ \mathbf{\downarrow} \mathbf{eval} \\ \boxed{d_0}[\mathbf{ret} \mathbb{t}] \end{array} $$

$$ c_0, g, c_1 \quad \mathbf{:=} \quad \mathbf{ret} \mathbb{t} $$

<caption>Figure 10: effectful interaction of u and $\gamma_o$.</caption>

* $\Delta_p, \Delta_o$ are two disjoint type contexts for effects and for-warded abstract delimited continuations.

* For $y \in \{o, p\}$. $\Gamma_y$ and $\Delta_y$ are disjoint.
The typing judgements $\mathfrak{E} \otimes \mathfrak{T}$ and $\mathfrak{P} \otimes \mathfrak{S}$ denotes that the configurations $\mathfrak{E}$ and $\mathfrak{P}$ are of type $\mathfrak{T}$ and $\mathfrak{S}$ respectively. We define the corresponding typing relation figure 11.

$$ \begin{array}{ccc} \text{PASSIVE CONF.} & & \\ \operatorname{dom}(\gamma) = \Gamma_p & \Gamma_o \vdash \gamma : \Gamma_p & \Gamma_p \vdash \xi : \Delta_o \\ & & \langle \mathbf{I}; \gamma; \xi \rangle \otimes \langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle \end{array} $$

$$ \begin{array}{ccc} \text{ACTIVE CONF.} & & \\ \operatorname{dom}(\gamma) = \Gamma_p & \mathbf{I}; \Gamma_o \cdot \Delta_o \vdash_c \mathbf{M} & \Gamma_o \vdash \delta : \Delta_p \\ & & \langle (\mathbf{M} | \mathbf{I}); \gamma; \delta \rangle \otimes \langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle \end{array} $$

<caption>Figure 11: configuration typing.</caption>

We will denote by $\mathfrak{T}^{\perp}$ the type configuration dual to $\mathfrak{T}$ defined by:

$$ \langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle^{\perp} := \langle \Gamma_p; \Delta_p | \Gamma_o; \Delta_o \rangle $$

The Type LTS $\mathcal{L}_T$ is defined as $(\mathcal{T}; \mathcal{M}; \mathbf{m} \xrightarrow{\cdot, T} \mathbf{m})$ with $\mathbf{m} \xrightarrow{\cdot, T}$ defined in figure 12, where $\mathcal{T}$ is the set of type configurations.

$$ \begin{array}{c} \text{PACTION} \\ \Gamma_o(\alpha) = \tau \\ \langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle \xrightarrow{\alpha, \alpha^{\oplus}} \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \end{array} $$

$$ \begin{array}{c} \text{PHANDLE} \\ \langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle^{\text{hdl}^{\oplus}} \xrightarrow{\text{hdl}^{\oplus}} \langle \Gamma_o; \Delta_o; \emptyset | \Gamma_p; \emptyset \rangle \end{array} $$

(a) proponent transitions.

$$ \frac{\mathfrak{T} \xrightarrow{\mathbf{m}} \mathfrak{S}}{\mathfrak{T}^{\perp} \xrightarrow{\mathbf{m}^{\perp}} \mathfrak{S}^{\perp}} $$

(b) symmetrical transitions.

<caption>Figure 12: Definition of $\mathcal{L}_T$</caption>

## 3.4 Well-bracketing Constraints

The interactive configurations $\mathfrak{I} \in \mathcal{A}$ we have considered thus far represent Proponent's one-sided perspective on the computation. The information component contains all of its codata that had been disclosed up to the current stage of the computation, namely the continuations. However, this component (and by extent any passive configuration), as it is defined, is history-agnostic whereas the language $\Lambda_{\text{eff}}$ only permits a constrained usage of these abstract continuations that respects a certain history-sensitive bracketing discipline.

In this section, we define the well-bracketing LTS that addresses this issue by constraining the moves of Opponent in $\mathcal{L}_{AI}$, so that the generated *well-bracketed* behaviours correspond to actual concrete interactions.

### 3.4.1 The control-flow of delimited continuations.
When an effect is performed by one *Player* and gets propagated beyond its immediate controlled scope, it initiates a sequence of effectful moves until the effect is handled or reaches *top-level*.

To visualise this part of the interaction, we will zoom in at the computation underlying it in the concrete example of 3.2.

<figure><img src="image_5.png" /><figcaption>Figure 13: effectful forward trace.</figcaption></figure>

In figure.13, we only highlight the player responsible for triggering the effect (in its active and passive states). The resulting effectful sequence is $d_1 \cdot \langle \kappa[e] | \square \rangle^{\oplus} c_0 \cdot \langle \kappa \vdash \kappa[e] | \square \rangle^{\ominus}$, which can be understood as a pseudo-copycat sequence in which Opponent forwards the computation $\langle e | d_1 \rangle \circ \kappa \rangle$ as is to the abstract continuation $c_0 \rangle$.

Now if we wish to generalize this sequence to one of arbitrary length $n$, $\mathfrak{I} \stackrel{s}{\Rightarrow} \text{fwd} \mathfrak{J}$, the generated configuration will always be of the following shape:

$$ \mathfrak{J} = \langle \langle \mathbf{t} \# \mathbf{o} \mathbf{p} \rangle \mid \mathfrak{T}[\{\mathbf{I}\}] \text{ with } \mathfrak{h} \rangle \circ \mathfrak{S}_{n+1}[\kappa_n[\mathfrak{S}_n[\dots \kappa_0[\mathfrak{S}_0]\dots]]] \mid \mathfrak{I} \rangle $$

Consequently, the captured continuation will be of the shape:

$$ \lambda x. (\{S_{n+1}[\kappa_n[S_n[\dots \kappa_0[S_0[\text{ret }x]]\dots]]\} \text{ with } \mathfrak{h}) $$

In the case the continuation is discarded and not used, the control-flow stack remains intact. Otherwise, every call to the captured delimited continuation entails exactly one query addressed to each one of the $n$ environment controlled fragments; i.e. a call to each of the abstract evaluation stacks $\kappa_i$ in the order in which they have been disclosed.

We define the well-bracketing LTS as $\mathcal{L}_{wb} := (\mathcal{W}, \mathcal{M}, \to_{wb})$ where the configurations are described below and the transitions
$m \xrightarrow{w_b} \mathbf{m}$ are defined in figure 14.

effect forwarding information

$\eta \quad ::= \quad \emptyset$ absence of effect
$\quad | \quad (f, e)$ effect e forwarded through f

configurations

$W, U := \langle \sigma | \eta | \phi \rangle$

where $\sigma \in \mathbf{List}(C \cup \mathcal{K})$, $f \in \mathcal{F} = \mathbf{List}(\mathcal{K})$ denote a control-flow stack and a call frame, respectively, and $\phi \in \wp(\mathcal{F})$ denotes the set of all captured call frames.

**REMARK 3.** In $\Lambda_{\text{eff}}$, arbitrary handlers can be defined as no restrictions are imposed on the usage of delimited continuations. This is reflected semantically in Opponent's transitions in $\mathcal{L}_{w_b}$, which permit unrestricted use of captured delimited continuation, thus allowing multi-shot continuations and re-entrant continuation calls.

In this setting, calling any captured delimited continuations only amounts to querying the top delimited continuation name $\kappa$ of the corresponding call frame $\kappa :: f$ and stacking the remainder $f$ on top of the control flow stack.

## 3.5 The OGS LTS

The OGS LTS ($O, M, \rightarrow_{ogs}$) is the transition system that can generate the interaction traces<fnref n="3" /> compatible with what our language ($\Lambda_{\text{eff}}$, $\mapsto_{op}$) permits.

It is defined as the product of $\mathcal{L}_{AI}$, $\mathcal{L}_{T}$ and $\mathcal{L}_{w_b}$ where the underlying labelled transitions systems are synchronised on $M \cup \{hdl^\oplus, hdl^\ominus\}$. The configurations in $O$ satisfy some conditions that guarantee the well-typedness of $\mathcal{L}_{AI}$; in that Opponent and Propponent agree on types during their interaction, in addition to ensuring that Opponent's use of continuations is well-bracketed.

In the following we will denote $\langle I \mid T \mid W \rangle \in \mathcal{A} \times \mathcal{T} \times \mathcal{W}$ any triple of configurations satisfying $I \perp T$ and $\mathbf{Comp}$($I, W$), where the second proposition morally means that the control-flow history in $W$ is compatible with the interactive information in $I$. The formal definition of this predicate will be later introduced in section D.2.

**3.5.1 Embedding the interactive language.** Finally, we define an interactive term embedding into an initial active $\mathcal{L}_{OGS}$ configuration and ciu-environment embedding into an initial passive $\mathcal{L}_{OGS}$ configuration.

**Definition 3.4 (term embedding).** Given an interactive term $I; \Gamma \vdash_c M$, we define its embedding

$$ \langle I; \Gamma \vdash_c M \rangle_{\text{ogs}}^{\oplus} := \langle \langle (M \mid I); \varepsilon \rangle \mid \langle \Gamma; \emptyset | c_f : \neg 1; \emptyset \rangle \mid \langle [d]; \emptyset; \emptyset \rangle \rangle $$

with $d$ the unique continuation name of $\Gamma$.

**Definition 3.5 (environment embedding).** Given a name assignment $I; c_f : \neg 1 \vdash \gamma : \Gamma$, we define its embedding

$$ \langle I; c_f : \neg 1 \vdash \gamma : \Gamma \rangle_{\text{ogs}}^{\ominus} := \langle \langle \emptyset; \gamma \rangle \mid \langle c_f : \neg 1; \emptyset | \Gamma; \emptyset \rangle \mid \langle [c_f]; \emptyset; \emptyset \rangle \rangle $$

# 4 THE OGS MODEL

## 4.1 Interpretation of expressions

Following our equivalence of programs introduced in definition 2.4, we only observe convergence, i.e. a full evaluation into a value

$$ \mathbf{forward}(\emptyset, c. \langle e | \Box \circ \kappa \rangle^{\ominus}) := (e, \emptyset) $$

$$ \mathbf{forward}(\emptyset, \kappa. \langle e | d[\Box] \circ \kappa \rangle^{\ominus}) := (e, \emptyset) $$

$$ \mathbf{forward}(\eta, \mathbf{o}) := \eta $$

$$ \mathbf{call}/\mathbf{ret}(\alpha \coloneqq \sigma, \lhd, \alpha, p^{\ominus}) := \sigma $$

$$ \mathbf{call}/\mathbf{ret}(\sigma, \phi, \kappa. \langle e | d[\Box] \circ r \rangle^{\ominus}) := f \oplus \sigma $$

$$ \mathbf{call}/\mathbf{ret}(\sigma, \phi, \kappa. \langle \text{ret} \vee | d[\Box] \rangle^{\ominus}) := f \oplus \sigma $$

$$ \text{when } \kappa \coloneqq f \in \phi $$

$$ \eta' = \mathbf{forward}(\eta, \mathbf{o}) \qquad \sigma' = \mathbf{call}/\mathbf{ret}(\sigma, \phi, \mathbf{o}) \\ \langle \sigma | \eta | \phi \rangle \xrightarrow{\circ} w_b \langle \sigma' | \eta' | \phi \rangle $$

$$ \langle \sigma | (e, f) | \phi \rangle \xrightarrow{hdl^{\ominus}} w_b \langle \sigma | \emptyset | \phi \cup \{f\} \rangle $$

(a) opponent transitions

$$ \mathbf{forward}((e, f), d. \langle e | \Box \circ \kappa \rangle^{\oplus}) := (f \oplus [\kappa], e) $$

$$ \mathbf{forward}((e, f), \kappa. \langle e | c[\Box] \circ \kappa \rangle^{\oplus}) := (f \oplus [\kappa], e) $$

$$ \mathbf{forward}(\emptyset, \mathbf{p}) := \emptyset $$

$$ \mathbf{call}/\mathbf{ret}(\sigma, \lhd, \kappa. \langle \text{ret} \vee | c[\Box] \rangle^{\oplus} ) := c \oplus \sigma $$

$$ \mathbf{call}/\mathbf{ret}(\sigma, \lhd, \kappa. \langle e | c[\Box] \circ \lhd \rangle^{\oplus} ) := c \oplus \sigma $$

$$ \mathbf{call}/\mathbf{ret}(\sigma, \lhd, f. \langle \Box \vee | c \rangle^{\oplus} ) := c \oplus \sigma $$

$$ \mathbf{call}/\mathbf{ret}(\sigma, \lhd, \mathbf{p}) := \sigma $$

$$ \sigma' = \mathbf{call}/\mathbf{ret}(\sigma, \mathbf{p}) \qquad \eta' = \mathbf{forward}(\eta, \mathbf{p}) \\ \langle \sigma | \eta | \phi \rangle \xrightarrow{\mathbf{p}} w_b \langle \sigma' | \eta' | \phi \rangle $$

$$ \langle \sigma | \emptyset | \phi \rangle \xrightarrow{hdl^{\ominus}} w_b \langle \sigma | \emptyset | \phi \rangle $$

(b) proponent transitions

<caption>Figure 14: $\mathcal{L}_{w_b}$ transitions.</caption>

returner of the shape $\mathbf{ret} \vee$. We introduce a notion of complete trace in order to capture this complete evaluation.

**Definition 4.1 (complete traces).** : A trace $t \mathbf{m} \in \mathbf{Tr}_{ogs}$ is said t be complete and written $\mathcal{CP}(t \mathbf{m})$ when:

$$ \mathcal{CP}(t \mathbf{m}) := \begin{cases} \langle [] | \emptyset | \emptyset \rangle & \mathbf{m} \stackrel{t \mathbf{m}}{\implies}_{w_b} \langle [] | \eta | \phi \rangle & \text{for some } \eta \text{ and } \phi \\ \mathbf{m} = c. \langle \mathbf{ret} \vee | \Box \rangle^{\ominus} & \text{for some } \mathbf{V} \text{ and } c. \end{cases} $$

Accordingly, we define the set of complete traces of a configuration:

$$ \mathrm{CT}_{\mathrm{ogs}}(\mathcal{G}) := \{t \in \mathrm{Tr}_{\mathrm{ogs}}(\mathcal{G}) | \mathcal{CP}(t)\} $$

## 4.2 Soundness of the model

**THEOREM 4.2 (ADEQUACY).** Given an interactive term $I; \Gamma \vdash_c M$ and a compatible name assignment

$I'; c_f : \neg 1 \vdash \gamma : \Gamma$, then by writing $\mathbf{P}$ and $\mathbf{E}$ for their respective ogs

<footnote n="3">³For a reader familiar with *game semantics*, this LTS specifies the *plays*.</footnote>
embeddings, we have:

$$ \exists I'' \supseteq I' \cdot I. (M\{\gamma\} | I' \cdot I) \Downarrow_{op} (c_f[\text{ret}(\langle\rangle)] | I'') \\ \iff \\ \exists t \in \text{CTr}_{\text{ogs}}(\mathbb{P}). t^{\perp} c_f \langle\text{ret}(\langle\rangle) | \Box\rangle^{\oplus} \in \text{CTr}_{\text{ogs}}(\mathbb{E}) $$

The proof of the previous adequacy theorem 4.2 is detailed in section B. It relies on the introduction of another LTS (cf. section A) that formalizes the notion of concrete interaction of example 3.2. This allows to define semantic notions of composition and observation (at the level of configurations and complete traces) which are then shown, in sections C and D, to coincide with their syntactic/- operational counterparts.

**THEOREM 4.3 (SOUNDNESS).** *Taking $M_1, M_2$ two interactive terms such that both $I; \Gamma \vdash_c M_i$ (for $i \in \{1, 2\}$), suppose that $\text{CTr}(\langle I; \Gamma \vdash M_1 \rangle) \subseteq \text{CTr}(\langle I; \Gamma \vdash M_2 \rangle)$. Then $\Gamma \vdash M_1 \leq_{ciu} M_2$.*

**PROOF.** We take a continuation name $c_f$, an instance context $I' \supseteq I$ and a name assignment $\gamma$ such that $I' : c_f : \neg 1 \vdash \gamma : \Gamma$. We write $\mathbb{G}_{P,i}$ for $\langle I; \Gamma \vdash_c T_i \rangle_{\text{ogs}}^{\oplus}$, and $\mathbb{G}_O$ for $\langle I'; c_f : \neg 1 \vdash \gamma : \Gamma \rangle_{\text{ogs}}^{\ominus}$.

Suppose that $(M_1\{\gamma\} | I') \Downarrow_{op} c_f[\langle\rangle]$. Then from theorem 4.2, we get the existence of a complete trace $t \in \text{CTr}(\mathbb{G}_{P,1})$ such that $t_1^{\perp} c_f \langle\text{ret}(\langle\rangle) | \Box\rangle^{\oplus} \in \text{CTr}(\mathbb{G}_O)$. From $\text{CTr}(\mathbb{G}_{P,1}) \subseteq \text{CTr}(\mathbb{G}_{P_2})$, we get that $t \in \text{CTr}(\mathbb{G}_{P,2})$. Finally, from theorem 4.2, we get that $(M_2\{\gamma\} | I') \Downarrow_{op} c_f[\langle\rangle]$, as we wanted. □

## 4.3 Counterexample to full-abstraction

The interaction of the term $u := \text{let } y = \text{new } \mathbb{E}$ in $\{f(\lambda x. y \# op(\langle\rangle))\}$ with $h^y$ (from example 3.2) with the environment $C := \text{let } f=(\lambda g. g \vdash \text{ret t})$ in $\llbracket$ was represented by the following trace we will denote by $s_u$,

$$ \mathbf{f} \langle \Box g | d \rangle^{\oplus} \mathbf{g} \langle \Box \vee c \rangle^{\ominus} \mathbf{c} \langle \kappa[e] | \Box \rangle^{\oplus} \mathbf{d} \langle \kappa_c : \kappa[e] | \Box \rangle^{\ominus} \mathbf{c}_c \langle \Box[\text{ret } 5] | d' \rangle^{\oplus} $$

Now considering the term $t := f(\lambda x.5)$, that is contextually equivalent to $u$, and observing how it interacts with the same environment $C$, we get:

$$ \begin{aligned} \langle c_f[t], \varepsilon, \emptyset \rangle & \xrightarrow{\mathbf{f} \langle \Box g | d \rangle^{\oplus}} \mathbf{1} & \langle [g \mapsto (\lambda x.5); d \mapsto c_f] \rangle; \emptyset \rangle \\ & \xrightarrow{\mathbf{g} \langle \Box \vee c \rangle^{\ominus}} \mathbf{1} & \langle c[(\lambda x.5)] \vee; [g \mapsto (\lambda x.5); d \mapsto c_f] \rangle; \emptyset \rangle \\ & \xrightarrow{\mathbf{c} \langle \text{ret } 5 | \Box \rangle^{\oplus}} \mathbf{1} & \langle [g \mapsto (\lambda x.5); d \mapsto c_f] \rangle; \emptyset \rangle \\ & \xrightarrow{\mathbf{d} \langle \text{ret } t | \Box \rangle^{\ominus}} \mathbf{1} & \langle c_f[\text{ret } t], [g \mapsto (\lambda x.5); d \mapsto c_f] \rangle; \emptyset \rangle \\ & \xrightarrow{\mathbf{c_f} \langle \text{ret } t | \Box \rangle^{\oplus}} \mathbf{1} & \langle [g \mapsto (\lambda x.5); d \mapsto c_f] \rangle; \emptyset \rangle \end{aligned} $$

that is an interaction witnessed by the trace $s_t$

$$ s_t = \mathbf{f} \langle \Box g | d \rangle^{\oplus} \mathbf{g} \langle \Box \vee c \rangle^{\ominus} \mathbf{c} \langle \text{ret } 5 | \Box \rangle^{\oplus} \mathbf{d} \langle \text{ret } t | \Box \rangle^{\ominus} \mathbf{c_f} \langle \text{ret } t | \Box \rangle^{\oplus} $$

It is clear that $s_u$ is not a trace generated by $t$, and $s_t$ is not a trace generated by $u$, so that their respective set of complete traces are incomparable. Therefore, a complete OGS model requires a notion of equivalence coarser than equality of traces, that would identify $s_t$ and $s_u$.

## 5 CONCLUSION AND RELATED WORK

We have provided a sound interactive model for a language with dynamically-scoped effect handlers and fresh generation of effect instances. Our model does not allow so far exchange of effect instances between the program and its environment, that would

necessitate to keep track of such disclosed instances in a specific set, to enforce a non-omniscience property as in [14]. The well-bracketing LTS would also have to keep track of the exchanged delimited continuations when the program performs a public effect (using a disclosed instance that is) because the environment, in this case, would be able to handle it, and thus its behaviour must be bound accordingly.

In future work, we will present a notion of equivalence between set of complete traces, coarser than equality, that we conjecture to be fully-abstract.

Game semantics has a long history of providing a fully-abstract interactive models for languages with control operators, starting from the relaxation of the well-bracketed condition by Laird to capture control operators like call/cc [20] and exceptions [21]. Game models for both statically bound, first-class continuations and locally declared, dynamically bound prompts were presented in [23], via a monadic presentation of such effects. In this work, prompts and exceptions cannot be referred by their names and passed around.

To represent them as values, nominal game semantics has been developed as a versatile framework to handle generative effects like dynamic name creation [1], higher-order references [29] and generative exceptions and handlers [30].

Operational techniques like applicative, normal-form and environmental bisimulations has also been developed for higher-order language with fine-grained control operators like static delimited continuations via shift and reset operations [6], dynamic ones via prompt and reset [4], and algebraic effects and handlers were considered in [7]. This last work is the most relevant to us, however they do not consider fresh generation of instances. Using a notion of Kripke normal-form bisimulations as introduced in [16, 19], that $\mathbf{f} \langle \Box g | d \rangle^{\oplus} \mathbf{g} \langle \Box \vee c \rangle^{\ominus} \mathbf{c} \langle \kappa_c : \kappa[e] | \Box \rangle^{\oplus} \mathbf{d} \langle \kappa_c : \kappa[e] | \Box \rangle^{\ominus} \mathbf{c} \langle \Box[\text{ret } 5] | d' \rangle^{\oplus}$ is directly derived from an OGS model, it would be interesting to explore the development of normal form bisimulations for such fresh generation of effect instances.

## REFERENCES

[1] Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong, and Ian David Bede Stark. 2004. Nominal Games and Full Abstraction for the Nu-Calculus. In *19th IEEE Symposium on Logic in Computer Science (LICS 2004)*, 14-17 July 2004, Turku, Finland, *Proceedings*. IEEE Computer Society, 150-159. https://doi.org/10.1109/LICS.2004.1319609

[2] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF. *Inf. Comput.* 163, 2 (dec 2000), 409-470. https://doi.org/10.1006/inco.2000.2930

[3] Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2014. Distilling Abstract Machines. In *Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14)*. Association for Computing Machinery, New York, NY, USA, 363-376. https://doi.org/10.1145/2628136.2628154

[4] Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2017. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. *Log. Methods Comput. Sci.* 13, 3 (2017). https://doi.org/10.23638/LMCS-13(3:27)2017

[5] Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. *Journal of Logical and Algebraic Methods in Programming* 84, 1 (2015), 108-123. https://doi.org/10.1016/j.jlamp.2014.02.001 Special Issue: The 23rd Nordic Workshop on Programming Theory (NWPT 2011) Special Issue: Domains X, International workshop on Domain Theory and applications, Swansea, 5-7 September, 2011.

[6] Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2019. Bisimulations for Delimited-Control Operators. *Log. Methods Comput. Sci.* 15, 2 (2019). https://doi.org/10.23638/LMCS-15(2:18)2019

[7] Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2020. A complete normal-form bisimilarity for algebraic effects and handlers. In *Formal Structures for Computation and Deduction*.

[8] Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2019. Binders by day, labels by night: effect instances via lexically scoped handlers.
*Proceedings of the ACM on Programming Languages* 4, POPL (2019), 1–29.

[9] Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as capabilities: effect handlers and lightweight effect polymorphism. *Proc. ACM Program. Lang.* 4, OOPSLA (2020), 126:1–126:30. https://doi.org/10.1145/3428194

[10] Vincent Danos, Hugo Herbelin, and Laurent Regnier. 1996. Game semantics and abstract machines. In *Proceedings 11th Annual IEEE Symposium on Logic in Computer Science*. IEEE, 394–405.

[11] Paulo Emílio de Vilhena and François Pottier. 2023. A type system for effect handlers and dynamic labels. In *Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings*. Springer Nature Switzerland Cham, 225–252.

[12] Matthias Felleisen and Robert Hieb. 1992. The Revised Report on the Syntactic Theories of Sequential Control and State. *Theoretical Computer Science* 103, 2 (Sept. 1992), 235–271. https://doi.org/10.1016/0304-3975(92)90014-7

[13] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The essence of compiling with continuations. *SIGPLAN Not.* 28, 6 (June 1993), 237–247. https://doi.org/10.1145/173262.155113

[14] Dan R Ghica and Nikos Tzevelekos. 2012. A system-level game semantics. *Electronic Notes in Theoretical Computer Science* 286 (2012), 191–211.

[15] Daniel Hillerström, Sam Lindley, and Robert Atkey. [n.d.]. Effect Handlers via Generalised Continuations. 30 ([n. d.]), e5. https://doi.org/10.1017/S0956796820000040

[16] Daniel Hirschkoff, Guilhem Jaber, and Enguerrand Prebet. 2023. Deciding Contextual Equivalence of v-Calculus with Effectful Contexts. In *Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 13992)*, Orna Kupferman and Pawel Sobocinski (Eds.). Springer, 24–45. https://doi.org/10.1007/978-3-031-30829-1_2

[17] J.M.E. Hyland and C.-H.L. Ong. 2000. On Full Abstraction for PCF. *Inf. Comput.* 163, 2 (dec 2000), 285–408. https://doi.org/10.1006/inco.2000.2917

[18] Guilhem Jaber and Andrzej S Murawski. 2021. Complete trace models of state and control. *Programming Languages and Systems* 12648 (2021), 348.

[19] Guilhem Jaber and Andrzej S. Murawski. 2021. Compositional relational reasoning via operational game semantics. In *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021*. IEEE, 1–13. https://doi.org/10.1109/LICS52264.2021.9470524

[20] James Laird. 1997. Full abstraction for functional languages with control. In *Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science*. 58–67. https://doi.org/10.1109/LICS.1997.614931

[21] James Laird. 2001. A Fully Abstract Game Semantics of Local Exceptions. In *16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings*. IEEE Computer Society, 105–114. https://doi.org/10.1109/LICS.2001.932487

[22] James Laird. 2007. A Fully Abstract Trace Semantics for General References. In *Proceedings of the 34th International Conference on Automata, Languages and Programming (Wroclaw, Poland) (ICALP'07)*. Springer-Verlag, Berlin, Heidelberg, 667–679.

[23] James Laird. 2017. Combining control effects and their models: Game semantics for a hierarchy of static, dynamic and delimited control effects. *Ann. Pure Appl. Log.* 168, 2 (2017), 470–500. https://doi.org/10.1016/J.APAL.2016.10.011

[24] P. J. Landin. 1964. The Mechanical Evaluation of Expressions. *Comput. J.* 6, 4 (Jan. 1964), 308–320. https://doi.org/10.1093/comjnl/6.4.308

[25] Søren B. Lassen and Paul Blain Levy. 2008. Typed normal form bisimulation for parametric polymorphism. In *2008 23rd Annual IEEE Symposium on Logic in Computer Science*. IEEE, 341–352.

[26] Paul Blain Levy. 2004. *Call-By-Push-Value: A Functional/Imperative Synthesis*. Semantics Structures in Computation, Vol. 2. Springer.

[27] Ian Mason and Carolyn Talcott. 1991. Equivalence in functional languages with effects. *Journal of Functional Programming* 1, 3 (1991), 287–327. https://doi.org/10.1017/S0956796800000125

[28] James Hiram Morris Jr. 1969. *Lambda-calculus models of programming languages*. Ph. D. Dissertation. Massachusetts Institute of Technology.

[29] Andrzej S Murawski and Nikos Tzevelekos. 2011. Game semantics for good general references. In *2011 IEEE 26th Annual Symposium on Logic in Computer Science*. IEEE, 75–84.

[30] Andrzej S Murawski and Nikos Tzevelekos. 2014. Game semantics for nominal exceptions. In *Foundations of Software Science and Computation Structures: 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings 17*. Springer, 164–179.

[31] Gordon Plotkin and John Power. 2001. Semantics for algebraic operations. *Electronic Notes in Theoretical Computer Science* 45 (2001), 332–345.

[32] Gordon Plotkin and John Power. 2002. Computational effects and operations: An overview. (2002).

[33] Gordon D Plotkin and Matija Pretnar. 2013. Handling algebraic effects. *Logical methods in computer science* 9 (2013).

[34] Yizhou Zhang and Andrew C. Myers. 2019. Abstraction-safe effect handlers via tunneling. *Proc. ACM Program. Lang.* 3, POPL (2019), 5:1–5:29. https://doi.org/10.1145/3290318
$I_a; \Gamma_o \vdash_c M$ and from lemma 2.2, we have $I'_a; \Gamma_o \vdash_c N$, thus $A' \otimes T^\perp$. The remaining complementarity conditions are trivially satisfied.

**Case** $\langle A \dashv\vdash P \rangle \stackrel{\text{hdl}}{\rightleftharpoons}_{\text{ci}} \langle A' \dashv\vdash P' \rangle$.

Then $A' = (\langle M | I_a \rangle; \gamma_p; \emptyset)$ and $P' = (\langle I_p; \gamma_a \cdot \delta_a \rangle \emptyset)$ where $\xi_a = (\_, \_, \delta_a)$.

Since $\text{supp}(M) \subseteq \text{dom}(\gamma_a) \cup \text{dom}(\delta_a)$ then $\text{supp}(M) \subseteq \text{dom}(\gamma'_a \delta_a)$.

W.l.o.g. let $T = \langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle$ and suppose $P \otimes \langle \Gamma_o; \Delta_o | \Gamma_p \cdot [c \mapsto \neg \tau]; \Delta_p \rangle^\perp$ and $A \otimes T$, Taking $S = \langle \Gamma_o \cdot \Delta_o; \emptyset | \Gamma_p; \emptyset \rangle$, since $I_a; \Gamma_o \cdot \Delta_o \vdash_c M$, we can verify that $A' \otimes S$ and $P \otimes \langle \Gamma_o \cdot \Delta_o; \emptyset | \Gamma_p \cdot [c \mapsto \neg \tau]; \emptyset \rangle^\perp$.

**Case** $\langle A \dashv\vdash P \rangle \stackrel{\text{dual}}{\rightleftharpoons}_{\text{ci}} \langle A' \dashv\vdash P' \rangle$.

By taking **abstract**(M, $\delta_p$) $\mathcal{R}$ ($\boldsymbol{\alpha}$.p, $\gamma_{\text{abs}}$, $\xi_p$) and writing **concretize**($\boldsymbol{\alpha}$.p, $\gamma_a; \xi_a$) = (N, $\delta_a$) with $N = \langle u | S' \circ T' \rangle$, we have $A' = (\langle N | I_p \rangle; \gamma_a; \delta_a)$ and $P' = (\langle I_a; \gamma_p \cdot \gamma_{\text{abs}}; \delta_p \cdot \xi \rangle)$.

We have that $\text{supp}(\text{codom}(\delta_a)) = \text{supp}(\text{codom}(\xi_a))$ and that $\text{supp}(\text{codom}(\xi)) \subseteq \text{supp}(t)$, thus by hypothesis, we have $\text{supp}(\text{codom}(\delta_a)) \subseteq \text{dom}(\gamma_p) \subseteq \text{dom}(\gamma_p \cdot \gamma_{\text{abs}})$, and we also have $\text{supp}(\text{codom}(\xi \cdot \delta_p)) \subseteq \text{supp}(\gamma_a)$.

W.l.o.g. let $T = \langle \Gamma_o; \Delta_o | \Gamma_p; \Delta_p \rangle$ and suppose $P \otimes \langle \Gamma_o; \Delta_o | \Gamma_p \cdot [c \mapsto \neg \tau]; \Delta_p \rangle^\perp$ and $A \otimes T$, Since $I_a; \Gamma_o \cdot \Delta_o \vdash_c M$ and $\alpha \in \text{dom}(\Gamma_o)$ (because $\alpha \in \text{supp}(t) \cup \text{supp}(S)$), then there exists $\tau$ s.t. $\Gamma_o(\alpha) = \tau$.

By writing $\Gamma_o \cdot \Delta_o \vdash_p p : \neg \tau \triangleright \Gamma_p; \Delta_p$ and taking $S = \langle \Gamma_p \cdot \Gamma_p; \Delta_p \cdot \Delta_p | \Gamma_o; \Delta_o \rangle$, it is easy to verify that $A' \otimes S$ and $P' \otimes \langle \Gamma_o; \Delta_o | \Gamma_p \cdot \Gamma_p \cdot [c \mapsto \neg \tau]; \Delta_p \cdot \Delta_p \rangle$.

□

In the following, we will use the notation $\langle P \dashv\vdash A \rangle$ to denote the couple $(P, A) \in \mathcal{A}^2$ satisfying $P \dashv\vdash A$.

### A.2.1 Concrete observation.
If an observation amounts to evaluating an observable value, an environment configuration can only do this after a switch of perspective, i.e through a $\stackrel{\text{dual}}{\rightleftharpoons}_{\text{ci}}$ transition. For this reason we will define the observation transition $\downarrow_{\text{ci}}$ a closure on $\stackrel{\text{dual}}{\rightleftharpoons}_{\text{ci}}$ (up-to $\stackrel{\text{eval}}{\rightleftharpoons}_{\text{ci}}$ and $\stackrel{\text{hdl}}{\rightleftharpoons}_{\text{ci}}$) such that $C \downarrow_{\text{ci}} D$ means $C \stackrel{\stackrel{\text{hdl}}{\rightleftharpoons}_{\text{ci}}}{\to}^* D$ where $C$ and $D$ are of opposite perspective.

#### Definition A.3.
Taking $\stackrel{\text{dual}}{\rightleftharpoons}$ to be $(\stackrel{\text{hdl}}{\rightleftharpoons}_{\text{ci}} \cup \stackrel{\text{eval}}{\rightleftharpoons}_{\text{ci}})^*$ $\stackrel{\text{dual}}{\rightleftharpoons}_{\text{ci}}$ $(\stackrel{\text{hdl}}{\rightleftharpoons}_{\text{ci}} \cup \stackrel{\text{eval}}{\rightleftharpoons}_{\text{ci}})^*$ we define:

$$C \downarrow_{\text{ci}} D :\iff \exists k \in \mathbb{N}. C \stackrel{2^k+1}{\rightleftharpoons} D \wedge D \not\vdash_{\text{ci}}$$

where, for $n \in \mathbb{N}$, $\stackrel{n}{\rightleftharpoons}_{\text{dual}} := \underbrace{\stackrel{\text{n times}}{\rightleftharpoons}}_{\text{dual} \cdots \stackrel{\text{n}}{\rightleftharpoons}_{\text{dual}}}$.

### A.2.2 Relating $\mathcal{L}_{\text{Al}}$ and $\mathcal{L}_{\text{Ci}}$.
We observe that, by definition, the interaction between a program and its environment given in the form of concrete interaction hides the parallel abstract composition of the underlying complementary passive and active $\mathcal{L}_{\text{Al}}$ configurations.

The following proposition captures how the $\stackrel{\text{eval}}{\rightleftharpoons}_{\text{ci}}$ transitions, can be equivalently re-expressed in terms of complementarity and the transition $\stackrel{\text{eval}}{\rightleftharpoons}_{\text{ci}}$.

### PROPOSITION A.4 (PARALLEL COMPOSITION).

$$\begin{array}{c} \text{EVALUATING} \\ \langle J \dashv\vdash I \rangle \stackrel{\text{eval}}{\rightleftharpoons}_{\text{ci}} \langle J \dashv\vdash I' \rangle \end{array}$$

$$\begin{array}{c} \text{HANDLING} \\ \langle J \dashv\vdash I \rangle \stackrel{\text{hdl}}{\rightleftharpoons}_{\text{ci}} \langle J \dashv\vdash I \rangle \end{array}$$

$$\begin{array}{c} \text{DUALIZING} \\ \langle J \dashv\vdash I \rangle \stackrel{\text{dual}}{\rightleftharpoons}_{\text{ci}} \langle K \dashv\vdash J \rangle \end{array}$$

#### COROLLARY A.5.
Given $I \in \text{Confs}_{\text{act}}$ and $J \in \text{Confs}_{\text{pas}}$ such that $I \dashv\vdash J$, we have:

$$\langle J \dashv\vdash I \rangle \stackrel{*}{\rightleftharpoons}_{\text{ci}} \langle J_0 \dashv\vdash J_1 \rangle \iff \exists t \in \text{Tr}_{\text{Al}}, i \in \{0, 1\}. J \stackrel{t}{\rightleftharpoons}_{i} J_0 \wedge I \stackrel{t^\perp}{\rightleftharpoons}_{i} J_1$$

$$\text{where } \stackrel{\text{m}}{\rightleftharpoons}_{i} := \stackrel{\text{hdl}}{\rightleftharpoons}_{i} \stackrel{*}{\text{eval}} \stackrel{\text{m}}{\rightleftharpoons}_{i} \stackrel{\text{hdl}}{\rightleftharpoons}_{i} \stackrel{*}{\text{eval}} \stackrel{\text{m}}{\rightleftharpoons}_{i}$$
# B ADEQUACY

Now that all the necessary definitions are available, we will state the main intermediate lemmas for proving adequacy: lemmas B.1 and B.2, and we will prove them in the following sections C and D, respectively.

**LEMMA B.1 (BISIMILARITY).** *Taking an interactive term $I_1; \Gamma \vdash_C M$ and a compatible name assignment $I'_1; d : \neg 1 \vdash \gamma : \Gamma$, then:*

$$ \langle I'_1, \gamma; \perp \dashv\vdash (M \mid I_1); \varepsilon, \perp \rangle \Downarrow_{ci} \langle I_2; \gamma_2; \perp \dashv\vdash (d[\mathbf{ret}(\langle\rangle)] \mid I'_2); \gamma_1; \perp \rangle \\ \iff \\ (M\{\gamma\} \mid I'_1 \cdot I_1) \Downarrow_{op} (d[\mathbf{ret}(\langle\rangle)] \mid I'_2 \cdot I_2) $$

**LEMMA B.2 (FULL OBSERVATION).** *Taking an interactive term $I; \Gamma \vdash_C M$ and a compatible name assignment $I'; d : \neg 1 \vdash \gamma : \Gamma$, then by writing $\mathbb{P}$ and $\mathbb{E}$ for their respective ogs embeddings, we have:*

$$ \exists \mathbb{K}, \gamma'. \langle \mathbb{J} \vdash \mathbb{I} \rangle \Downarrow_{ci} \langle \mathbb{K} \vdash \mathbb{d}[\mathbf{ret}(\langle\rangle)]; \gamma'; \perp \rangle \\ \iff \\ \exists t \in \mathbf{CT}_{ogs}(\mathbb{G}). \quad t^{\perp} \mathbf{d} \langle \mathbf{ret}(\langle\rangle) | \Box \rangle^{\oplus} \in \mathbf{CT}_{ogs}(\mathbb{H}) $$

**THEOREM B.3 (ADEQUACY).** *Given an interactive term $I; \Gamma \vdash_C M$ and a compatible name assignment $I'; d : \neg 1 \vdash \gamma : \Gamma$, then by writing $\mathbb{P}$ and $\mathbb{E}$ for their respective ogs embeddings, we have:*

$$ ((M\{\gamma\} \mid I' \cdot I) \Downarrow_{op} (d[\mathbf{ret}(\langle\rangle)] \mid I'') \\ \iff \\ \exists t \in \mathbf{CT}_{ogs}(\mathbb{P}). \quad t^{\perp} \mathbf{d} \langle \mathbf{ret}(\langle\rangle) | \Box \rangle^{\oplus} \in \mathbf{CT}_{ogs}(\mathbb{E}) $$

**PROOF.** Follows from the two preceding lemmas. $\square$

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

# C BISIMILARITY (PROOF OF LEMMA B.1)

($\mathcal{L}_{ci}, \mapsto_{ci}$) AND ($\Lambda_{eff}, \mapsto_{op}$) ARE WEAKLY BISIMILAR

We start by stating the main result of this section; that is modulo $\dual \mapsto_{ci}$ and $\dual \mapsto_{ci}$ reductions, the transition systems ($\mathcal{L}_{ci}, \mapsto_{ci}$) and ($\Lambda_{eff}, \mapsto_{op}$) are realted by a weak bisimulation. Afterwards we will introduce the necessary definitions and lemmas in order to prove it.

The proof relies on a notion of telescoped substitution to avoid cycles in the concatenation of mappings coming from the composition of two interactive configurations. This enforces the absence of livelocks in the interaction.

**Definition C.1.** A telescoped substitution $\delta$ is a substitution seen as a stack of mappings $[\alpha_0 \mapsto v_0, \dots, \alpha_k \mapsto v_k]$ such that for all $i \in \{1, \dots, k\}$, we have $\mathrm{supp}(v_i) \cap \{\alpha_i, \dots, \alpha_k\} = \emptyset$.

**PROPOSITION C.2.** *Given a telescoped substitution $[\alpha_0 \mapsto v_0, \dots, \alpha_k \mapsto v_k]$, for all $i \in \{1, \dots, k\}$, we have $\mathrm{supp}(v_i) \subseteq \{\alpha_0, \dots, \alpha_k\}$.*

A telescoped substitution $\delta$ can be transformed into a substitution $\delta^*$ such that for any $\alpha \in \mathrm{dom}(\delta) \mathrm{supp}(\delta(\alpha)) \subseteq \mathrm{supp}(v_0)$.

**Definition C.3.** Taking a telescoped substitution $\delta$ and $k \in \mathbb{N}^*$, we define the iterated telescoped substitution $\delta^i$ as:

$$ \delta^1 := \delta \qquad \delta^{i+1} := \Pi_{n \in \mathrm{dom}(\delta)} [n \mapsto \delta(n)\{\delta^i\}] $$

We then define $\delta^*$ as $\delta^k$ with $k$ the size of the domain of $\delta$. Then if $\Gamma \cdot \Delta \vdash \delta : \Gamma$ and $\mathrm{dom}(\Delta) = \mathrm{supp}(v_0)$, we have $\Delta \vdash \delta^* : \Gamma$.

**LEMMA C.4.** *Taking a telescoped substitution $\delta$ and $\alpha \in \mathrm{dom}(\delta)$, then there exists a name $\alpha \in \mathrm{dom}(\delta)$ and a natural number $k \in \mathbb{N}^*$ such that $\mathrm{supp}(\delta^k(\alpha)) \cap \mathrm{dom}(\delta) = \emptyset$.*

We define a bisimulation between $\mapsto_{ci}$ and $\mapsto_{op}$ by collapsing $\mathcal{L}_{ci}$ configurations into operational ones.

**LEMMA C.5.** Let $\langle \mathbb{E} \vdash \mathbb{P} \rangle \in \mathrm{Confs}_{ci}$ such that $\mathbb{E} \vdash_d \mathbb{P}$. If we write $\mathbb{E} = \langle I_p; \gamma_p; \xi_p \rangle$ and $\mathbb{P} = \langle (M \mid I_a); \gamma_a; \delta_a \rangle$ and $\mathbb{P} \not\vdash \langle \Gamma_o; \Delta_o \mid \Gamma_p; \Delta_p \rangle$, then $\delta = \gamma_a \cdot \gamma_p$ is a telescoped substitution, and there exists $I_a \cdot I_p; d : \neg 1 \vdash \delta^* : \Gamma_p \cdot \Gamma_o$.

**Definition C.6.** We define the function $\Phi_{op}^{ci} : \mathrm{Confs}_{ci} \to \Lambda_{eff}$ as the function:

$$ \langle I_p; \gamma_p; \xi_p \vdash (M \mid I_a); \gamma_a; \delta_a \rangle \mapsto (M\{(\gamma_p \cdot \gamma_a)^* \cdot \delta_e\} \mid I_p \cdot I_a) $$

with

$$ \delta_e := \begin{cases} \varepsilon & \text{if } \xi_p = \perp \\ \delta_a \cdot \delta_p & \text{if for some } Y \in \{a, p\}, \quad \xi_p =! (e, \_ \cdot \delta_p) \end{cases} $$

We write $\mathcal{B}_{op}^{ci}$ for the functional relation corresponding to $\Phi_{op}^{ci}$.

**LEMMA C.7.** If $\mathbb{C} \stackrel{\mathrm{dual}}{\mapsto_{ci}} \mathbb{D}$ or $\mathbb{C} \stackrel{\mathrm{hdl}}{\mapsto_{ci}} \mathbb{D}$, then $\Phi_{op}^{ci}(\mathbb{C}) = \Phi_{op}^{ci}(\mathbb{D})$.

**PROOF.** We proceed by case analysis knowing that $\mathbb{C} = \langle I_p; \gamma_p; \xi_p \vdash (P(\alpha) \mid I_a); \gamma_a; \delta_a \rangle$ and that $\mathbb{P}(\alpha)$ is in normal form. $\square$

**LEMMA C.8.** Taking a configuration $\mathbb{C} \in \mathrm{Confs}_{ci}$, there exists a configuration $\mathbb{D}$ such that $\mathbb{C} \stackrel{\mathrm{dual}}{\mapsto_{ci}} * \mathbb{D}$ and $\mathbb{D} \stackrel{\mathrm{dual}}{\mapsto_{ci}} * \mathbb{D}$.

**PROOF.** Let's write $\mathbb{C}$ as $\langle I_p; \gamma_p; \xi_p \vdash (M \mid I_a); \gamma_a; \delta_a \rangle$ and $\gamma = [\alpha_0 \mapsto v_0, \dots, \alpha_n \mapsto v_n]$ for $\gamma_a \cdot \gamma_p$.

If $M$ is not in normal form then $\mathbb{C} \stackrel{\mathrm{dual}}{\mapsto_{ci}}$, thus $\mathbb{D} = \mathbb{C}$. Otherwise, there exists an index $k \in \{0, \dots, n\}$ and a copattern, whose shape is either $\langle \Box \mid S \rangle$ or $\langle \_ \mid S[\Box] \circ \_ \rangle$, such that $M = P(\alpha_k)$. We proceed by induction on $k$ and on the length of $S$.

**case M** $= \langle f \mid S \rangle$ with $f \in \mathrm{dom}(\gamma)$.

**Subcase $\gamma(f) \in \mathrm{dom}(\gamma)$**.

Since $\gamma$ is a telescoped substitution, there exists $\ell \in \{k+1, \dots, n\}$ such that $\gamma(f) = \alpha_\ell$. Thus there exists a configuration $\mathbb{D}$ such that $\mathbb{C} \stackrel{\mathrm{dual}}{\mapsto_{ci}} \mathbb{C}'$ and whose active component can be written as $\langle d[\alpha_\ell \mathbb{V}] ; \gamma_p \cdot \gamma_v ; \emptyset \rangle$. By induction hypothesis, there exists $\mathbb{D}$ such that $\mathbb{C}'(\stackrel{\mathrm{dual}}{\mapsto_{ci}})^*\mathbb{D}$, and in particular $\mathbb{C}'(\stackrel{\mathrm{dual}}{\mapsto_{ci}})^*\mathbb{D}$, and $\mathbb{D} \stackrel{\mathrm{dual}}{\mapsto_{ci}} \mathbb{D}$.

**Subcase $\gamma(f) \notin \mathrm{dom}(\gamma)$**.

$\gamma(f)$ is a $\lambda$-abstraction. Then there exists a configuration $\mathbb{D}$ such that $\mathbb{C} \stackrel{\mathrm{dual}}{\mapsto_{ci}} \mathbb{D}$ and whose active component can be written as $\langle d[(\lambda x.t) \mathbb{V}] ; \gamma_p \cdot \gamma_v ; \emptyset \rangle$. From which we can deduce that $\mathbb{D} \stackrel{\mathrm{op}}{\mapsto_{ci}}$ and in particular that $\mathbb{D} \stackrel{\mathrm{dual}}{\mapsto_{ci}} \mathbb{D}$.

**case M** $= \langle \mathbf{ret} \mid S[\kappa[\mathbb{V}]] \rangle \langle e \mid S[\kappa[\mathbb{V}]] \circ S \rangle$ with $\kappa \in \mathrm{dom}(\gamma)$.
**Subcase** $\gamma(\kappa) = T[E]$.

Then there exists a configuration $\mathcal{D}$ such that $C \underset{\text{ci}}{\overset{\text{dual}}{\to}} \mathcal{D}$ and whose active term $N$ can be written as $\langle \text{ret} \ \mathcal{V} \ | \ S[\text{T}[E]] \rangle$ in which case $N \mapsto_{\text{eval}}$, or as $\langle e\{\delta_p\} \ | \ S[\text{T}[E]] \circ S \rangle$ in which case $N \mapsto_{\text{fwd}}$. In either case, we have $\mathcal{D} \underset{\text{ci}}{\overset{\text{op}}{\to}}$ and in particular that $\mathcal{D} \underset{\text{ci}}{\overset{\text{dual}}{\to}}$.

**Subcase** $\gamma(\kappa) = \square$.

Suppose $M = \langle \text{ret} \ \mathcal{V} \ | \ S[\kappa[\mathcal{I}]] \rangle$, we have

$$ C \underset{\text{ci}}{\overset{\text{dual}}{\to}} \langle I_a; \gamma_a; \emptyset \dashv \langle \text{ret} \ \mathcal{V} \ | d[\mathcal{I}] \rangle; \gamma_p \cdot \gamma_v \cdot [d \mapsto S]; \emptyset \rangle \\ \underset{\text{ci}}{\overset{\text{dual}}{\to}} \langle I_p; \gamma_p \cdot \gamma_v \cdot \gamma_d; \emptyset \dashv \langle \text{ret} \ \mathcal{W} \ | S \ | I_a \rangle; \gamma_a \cdot \gamma_w; \emptyset \rangle = C' $$

We conclude by applying the induction hypothesis on $C'$. The same reasoning applied to the other case.

**case** $M ::= \langle \text{ret} \ \mathcal{V} \ | c[\mathcal{I}] \rangle | \langle e \ | c[\mathcal{I}] \circ S \rangle$.

**Subcase** $c \notin \text{dom}(\gamma)$ Then $\mathcal{D} = \mathcal{C}$ since $C \underset{\text{ci}}{\overset{\text{dual}}{\to}}$.

**Subcase** $\gamma(c) ::= \gamma(c) = \alpha_\ell[\mathcal{I}]$ with $\ell \in \{k+1, \dots, n\}$.

There exists a configuration $C'$ such that $C \underset{\text{ci}}{\overset{\text{dual}}{\to}} C'$ and whose active component can be written as $\langle (Q(\alpha_\ell) | I_p); \gamma_p \gamma_0; \emptyset \rangle$ where $Q$ is a copattern. We conclude using the induction hypothesis on $C'$.

□

**LEMMA C.9.** Let $I; \Gamma \Vdash_c M$ be an interactive computation and let $I; \Delta \vdash \gamma : \Gamma$ be a name assignment.

If $(M | I) \mapsto_{\text{op}} (N | I')$ then $(M\{\gamma\} | I) \mapsto_{\text{op}} (N\{\gamma\} | I')$.

**LEMMA C.10.** Let $I; \Gamma \Vdash_c M$ be a computation s.t. $(M | I) \mapsto_{\text{op}}$ and let $I; \Delta \vdash \gamma : \Gamma$ be a name assignment.

If $(M\{\gamma\} | I) \mapsto_{\text{op}} (N\{\gamma\} | I')$ and $\text{supp}(M) = \text{supp}(N)$, then $(M | I) \mapsto_{\text{op}} (N | I')$.

**PROOF.** By case analysis knowing that any such term $M$ is given by the syntax:

$$ \begin{array}{l} \text{Nf}_{\text{fwd}} ::= \langle \text{ret} \ \mathcal{V} \ | S[E] \rangle | \langle (\lambda x.t) \ \mathcal{V} \ | S \rangle \\ \phantom{\text{Nf}_{\text{fwd}} ::=} | \langle t \# \text{op} \ \mathcal{V} \ | S[\mathcal{I}] \rangle \text{ with } h \circ S \rangle \quad (t \in \text{hdl}(h)) \\ \phantom{\text{Nf}_{\text{fwd}} ::=} | \langle e \ | S[E] \circ S \rangle \end{array} $$

□

**LEMMA C.11.** Taking a configuration $C \in \text{Confs}_{\text{ci}}$ s.t. $\Phi_{\text{op}}^{\text{ci}}(C) \mapsto_{\text{op}} (N | I)$, then there exists a configuration $\mathcal{D} \in \text{Confs}_{\text{ci}}$ s.t. $C \underset{\text{ci}}{\overset{\text{dual}}{\to}} \mathcal{D}$ and $\Phi_{\text{op}}^{\text{ci}}(\mathcal{D}) = (N | I)$.

**PROOF.** Let's write $C = \langle I_p; \gamma_p; \xi_p \dashv (M | I_a); \gamma_a; \delta_a \rangle$.

**Case** $C \underset{\text{ci}}{\overset{\text{dual}}{\to}}$; that is $M \notin \text{Nf}(\Lambda_{\text{eff}})$.

By hypothesis, we have $\Phi_{\text{op}}^{\text{ci}}(C) = (M\{\gamma\} | I_p \cdot I_a) \mapsto_{\text{op}} (N'\{\gamma\} | I)$ where $\gamma = (\gamma_p \cdot \gamma_a)^*$ and $N'$ is such that $\text{supp}(M) = \text{supp}(N')$ and $M = N'\{\gamma\}$. Then from lemma C.10, we can deduce that $C \underset{\text{ci}}{\overset{\text{op}}{\to}} \langle I_p; \gamma_p; \emptyset \dashv (N' | I'_a); \gamma_a; \emptyset \rangle = \mathcal{D}$ where $I = I_p \cdot I'_a$, which entails that $\Phi_{\text{op}}^{\text{ci}}(\mathcal{D}) = (N'\{\gamma\} | I_p \cdot I'_a) = (N | I)$.

**Case** $C \underset{\text{ci}}{\overset{\text{dual}}{\to}}$.

By lemma C.8, there exists $C'$ s.t. $C \underset{\text{ci}}{\overset{\text{dual}}{\to}} C'$ and $C' \underset{\text{ci}}{\overset{\text{dual}}{\to}}$.

□

**LEMMA C.12 (BISIMULATION).** Taking $\Rightarrow_{\text{ci}} := (\underset{\text{ci}}{\stackrel{\text{hdl}}{\to}})^* \Rightarrow_{\text{ci}}$ and $\Rightarrow_{\text{ci}} := (\underset{\text{ci}}{\stackrel{\text{dual}}{\to}})^* \Rightarrow_{\text{ci}}$, there exists a bisimulation relating $(\text{Confs}_{\text{ci}}, \Rightarrow_{\text{ci}})$ and $(\Lambda_{\text{eff}}, \Rightarrow_{\text{op}})$, i.e there exists a relation $\mathcal{B}_{\text{op}}^{\text{ci}} \in \wp(\text{Confs}_{\text{ci}} \times \Lambda_{\text{eff}})$ s.t. the following diagram holds.

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

**PROOF.** We show that $\mathcal{B}_{\text{op}}^{\text{ci}}$ and its converse are simulations.

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

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

□

**COROLLARY C.13.** Taking a nominal term $I; \Gamma; \emptyset \vdash_c t : \tau$, a compatible evaluation context $I'$; $\Delta \vdash E : \tau \rightsquigarrow 1$ and a assignment
I'; Δ ⊢ γ : Γ, then:

`⟨I'₁, γ · [c ↦→ d[E]]; ⊥ ⊎ (c[t] | I₁); ε, ⊥⟩ ⇝ ci ⟨I₂; γ₂; ⊥ ⊎ (d[ret ⟨⟩] |`

⇔

`(E[t{γ}] | I'_1 · I_1) ⇝_{op} (d[ret ⟨⟩] | I'_2 · I_2)`

D OBSERVATION (PROOF OF LEMMA B.2)

D: y₁; Relating (L<sub>T</sub>, →<sub>T</sub>) to (L<sub>A|I</sub> →<sub>I</sub>)

LEMMA D.1. Taking a well-typed interactive term in normal form
I; Γ ⊢<sub>c</sub> Nf such that
abstract(Nf, δ) ⇝<sub>Π</sub> (α,q, γ, δ·ξ) and Γ(α) = τ and Γ ⊢<sub>p</sub> q : ¬τ ⊲
Γ<sub>q</sub>; Δ<sub>q</sub>, we have: Γ ⊢ γ : Γ<sub>q</sub> and Γ ⊢ ξ : Δ<sub>q</sub>.

LEMMA D.2. Given a well-typed interactive term I; Δ·Γ ⊢<sub>c</sub> M and a substitution Γ' ⊢ δ : Δ such that Γ' ⊆ Γ and dom(Δ) ⊆ dom(δ), then: I; Γ ⊢<sub>c</sub> M{δ}

LEMMA D.3 (SUBJECT REDUCTION). Taking I, J ∈ 𝒜 and T ∈ 𝒯 such that I ⊢_S T and I ↦_1 J, then there exists T ∈ 𝒯 such that T ↦_T S and J ⊢ S.

PROOF. We write T = ⟨Γ₀; Δ₀ | Γₚ; Δₚ⟩ and proceed by case analysis on α.

Case $\alpha = hdl^\oplus$.

Then if we take I = ⟨(M | I); γ; !δ⟩, we have I $\xrightarrow{hdl^\oplus}$ I1 ⟨(M | I); γ; Ø⟩ = J. It is immediate to verify that S = ⟨Γ₀ · Δ₀; Ø | Γₚ; Ø⟩ is s.t. T $\xrightarrow{hdl^\oplus}$ₜ S and J ⊢ S.

Case $\alpha = hdl^\ominus$.

Then if we take I = ⟨I; γ; ?ξ⟩ where ξ = (__, δ), we have
I $\xrightarrow{hdl^\oplus}$ I1 ⟨I; γ·δ; Ø⟩ = J. Similarly, it is immediate to verify
that S = ⟨Γ₀; Ø | Γₚ·Δₚ; Ø⟩ is s.t. T $\xrightarrow{hdl^\oplus}$ₜ S and J ⊢ S.

Case $\alpha = \alpha.p^\oplus$.

Then if we write I = ⟨(Nf | I); γ; δ⟩, we have I $\xrightarrow{\alpha.p^\oplus}$ I1
⟨I; γ·γ<sub>abs</sub>; ξ⟩ = J with abstract(Nf, δ) ⇝ (γ<sub>abs</sub>, δ·ξ).
Since I ⊢ T, we have I; Γ₀·Δ₀ ⊢<sub>c</sub> Nf, and since α ∈ supp(Nf)
then there exists τ, Γₚ, Δₚ such that Γ₀(α) = τ and Γ₀·Δₚ·
Δ₀ ⊢ₚ p : ¬τ ⊲ Γₚ; Δₚ, so by lemma D.1, we have Γ₀ ⊢ γ<sub>abs</sub> : Γₚ
and Γ₀·Δ₀ ⊢ ξ : Δₚ.

Thus by taking $\mathcal{S} = \langle \Gamma_o; \Delta_o | \Gamma_p \cdot \Delta_p; \Delta_p \cdot \Delta_p \rangle$, it is immediate
that $\mathcal{T} \xrightarrow{\alpha.p^\oplus} \mathcal{T} \mathcal{S}$ and $\mathcal{J} \otimes \mathcal{S}$, knowing that $I; \Gamma_o \vdash \gamma : \Gamma_p$, and
$I; \Gamma_o \vdash \delta : \Delta_p$.

Case $\alpha = \alpha.p^\ominus$.

Then if we take I = ⟨I; γ; ξ⟩ where ξ = (__, δ), we have
I $\xrightarrow{\alpha.p^\ominus}$ I1 ⟨(M | I); γ; δ⟩ = J where M = p{δ}(γ(α)).

Let $\tau$, $\Gamma_p$, $\Delta_p$ such that $\Gamma_p(\alpha) = \tau$ and $\Delta_p \cdot \Delta_o \vdash_p p : \neg \tau \vdash$
$\Gamma_p; \Delta_p$, then we have $\mathcal{T} \xrightarrow{\alpha.p^\oplus} \Gamma \vdash_T \langle \Gamma_o \cdot \Gamma_p; \Delta_o \cdot \Delta_p | \Gamma_p; \Delta_p \rangle = \mathcal{S}$.
Since $\mathcal{I} \not\vdash_T$, we have $\mathcal{I}; \Gamma_o \vdash \gamma : \Gamma_p$ and $\mathcal{I}; \Gamma_o \vdash \delta : \Delta_p$ and in
particular $\mathcal{I}; \Gamma_o \vdash \Gamma_p \vdash \gamma : \Gamma_p$ and $\mathcal{I}; \Gamma_o \vdash \Gamma_p \vdash \delta : \Delta_p$.
Moreover, since $\mathcal{I}$; $[\alpha \mapsto \tau] \cdot \Gamma_p \cdot \Delta_p \cdot \Delta_o \cdot \Delta_p \vdash_c p(\alpha)$ and
$\mathrm{dom}(\Delta_o) = \mathrm{dom}(\delta)$, then by lemma D.2 we have $\mathcal{I}$; $[\alpha \mapsto \tau] \cdot \Gamma_p \cdot \Delta_o \cdot \Delta_p \vdash_c p(\delta)(\alpha)$. Finally, given that $\mathcal{M} = p(\delta)(\alpha)$ and
$\Gamma_o \vdash \gamma(\alpha) : \tau$ then we can deduce that $\mathcal{I}; \Gamma_o \cdot \Gamma_p \cdot \Delta_o \cdot \Delta_p \vdash_c \mathcal{M}$,
and by extent $\mathcal{J} \not\vdash_S$.

□

D.2 Compatibility of ($\mathcal{L}_{A|I}$, →$_1$) and ($\mathcal{L}_{wb}$, →$_{wb}$)

Definition D.4. We define the predicate ∧□ on {?, !} × 𝒩 × F,
relating an *abstract forward stack* to a *call frame*, depending on
which *player* has performed the effect.

$$ \frac{\begin{array}{c} \cdot \wedge? [] \\ r \wedge? f \end{array}}{r \wedge? \wedge \kappa \wedge \Lambda? \kappa \wedge f} $$

$$ \frac{\begin{array}{c} \cdot \wedge! [] \\ r \wedge! f \end{array}}{r \wedge? \wedge \kappa \wedge \Lambda? \kappa' \wedge f} $$

**Definition D.5** ( $(\mathcal{L}_{AI}, \mathcal{L}_{w6})$-compatibility). Let $\mathbb{I}, \mathbb{J} \in \mathcal{A}$ and $\mathbb{W} \in \mathcal{W}$ s.t. $\mathbb{I} = \langle \gamma; \xi \rangle, \mathbb{J} = \langle \langle t | S \circ S | I \rangle; \gamma'; \delta \rangle$ and $\mathbb{W} = \langle \sigma | \eta | \phi \rangle$.

We say that $\mathbb{I}$ and $\mathbb{W}$ are compatible when $\mathbf{Compat}(\mathbb{I}, \mathbb{W})$ holds, where

$$ \mathbf{Compat}(\mathbb{I}, \mathbb{W}) \iff \forall \mathfrak{f} \in \phi. \mathbf{set}(\mathfrak{f}) \subseteq \mathbf{dom}(\gamma) \wedge \xi \sim \mathbf{fwd} \eta $$

Similarly, we say that $\mathbb{J}$ and $\mathbb{W}$ are compatible when $\mathbf{Compat}(\mathbb{J}, \mathbb{W})$ holds, where

$$ \mathbf{Compat}(\mathbb{J}, \mathbb{W}) \iff \forall \mathfrak{f} \in \phi. \mathbf{set}(\mathfrak{f}) \subseteq \mathbf{dom}(\gamma') \wedge \delta \sim \mathbf{fwd} \eta $$

with

$$ \emptyset \sim \mathbf{fwd} \emptyset \quad ! (e, \_, \_) \sim \mathbf{fwd} (\emptyset, e) \quad ? (e, r, \_) \sim \mathbf{fwd} (f, e) \text{ when } r \wedge? f $$

$$ ! \delta^e \sim \mathbf{fwd} (\emptyset, e) \quad ? \delta \sim \mathbf{fwd} (f, e) \text{ when } r \wedge? f \text{ and } S\{\delta^{-1}\} = \mathbb{T} \oplus r $$

**LEMMA D.6** (PRESERVATION OF COMPATIBILITY). Let $\mathbb{I} \in \mathcal{A}$ and $\mathbb{W} \in \mathcal{W}$ s.t. $\mathbf{Compat}(\mathbb{I}, \mathbb{W})$.

If $\mathbb{I} \xrightarrow{\alpha} \mathbb{J}$ and $\mathbb{W} \xrightarrow{\alpha} \mathbb{w}_6 \mathbb{U}$, then $\mathbf{Compatible}(\mathbb{I}, \mathbb{U})$.

**PROOF.** We write $\mathbb{W} = \langle \sigma | \eta | \phi \rangle$ with $\eta = (e, f)$ then proceed by case analysis on $\mathbb{I}$ and $\alpha$.

$$ \mathbf{Case} \ \mathbb{I} = \langle \mathbb{I}; \gamma; \Box \xi \rangle \text{ with } \Box \in \{?, !\} \text{ and } \xi = (e, r, \delta). $$

$$ \mathbf{Subcase} \ \alpha = \mathbf{hdl}^{\alpha}. $$

By hypothesis, we have $r \wedge? f$ and $\forall f' \in \phi$. $\mathbf{set}(f') \subseteq \mathbf{dom}(\gamma)$. Moreover, we have $\mathbb{J} = \langle \mathbb{I}; \gamma \cdot \delta; \emptyset \rangle$ and $\mathbb{U} = \langle \sigma | \emptyset | \phi \cup \{f\} \rangle$, thus, since $\mathbf{set}(f) \subseteq \mathbf{dom}(\delta)$ we can deduce that $\forall f' \in \phi \cup \{f\}$. $\mathbf{set}(f') \subseteq \mathbf{dom}(\gamma \cdot \delta)$ and $\emptyset \sim \mathbf{fwd} \emptyset$, from which we can conclude that $\mathbf{Compatible}(\mathbb{J}, \mathbb{U})$.

$$ \mathbf{Subcase} \ \alpha ::= \mathbf{c.} \langle \mathbf{ret} \ \mathbb{V} \mid \Box \rangle^{\circ} \mid \mathbf{k.} \langle \Box \ \mathbf{ret} \ \mathbb{V} \mid \mathbb{V} \rangle^{\circ} \mid \mathbf{d}^{\circ} \rangle^{\circ} \mid \mathbf{f.} \langle \Box \ \mathbb{V} \mid \mathbb{d} \rangle^{\circ} \rangle^{\circ}. $$

In either subcase, there exist $\mathbb{M}$ and $\sigma'$ s.t. $\mathbb{J} = \langle (\mathbb{M} | \mathbb{I}); \gamma; \emptyset \rangle$ and $\mathbb{U} = \langle \sigma' | \emptyset | \phi \rangle$. Moreover, by defintion $\emptyset \sim \mathbf{fwd} \emptyset$, and by hypothesis we have $\forall f \in \phi$. $\mathbf{set}(f) \subseteq \mathbf{dom}(\gamma)$, thus $\mathbf{Compatible}(\mathbb{J}, \mathbb{U})$.

$$ \mathbf{Subcase} \ \alpha ::= \mathbf{c.} \langle \kappa[e] \mid \Box \rangle^{\circ} \mid \kappa'. \langle \Box[\kappa[e]] \mid \mathbb{d} \rangle^{\circ} \text{ (performing an effect)}. $$

In either subcase, there exist $\mathbb{S}$, $\sigma'$ s.t. $\mathbb{J} = \langle \langle e | S \circ \kappa | \mathbb{I} \rangle; \gamma; \varepsilon \rangle$ and $\mathbb{U} = \langle \sigma' | (e, \mathbb{I}) | \phi \rangle$.

We have then, by definition, $\kappa \wedge? []$ and $? \varepsilon \sim \mathbf{fwd} (e, \mathbb{I})$, and by hypothesis, we have that $\forall f \in \phi$. $\mathbf{set}(f) \subseteq \mathbf{dom}(\gamma)$. Thus, we can conclude that $\mathbf{Compatible}(\mathbb{J}, \mathbb{U})$.

$$ \mathbf{Subcase} \ \alpha ::= \mathbf{c.} \langle \kappa : r[e] \mid \Box \rangle^{\circ} \mid \kappa'. \langle \Box[\kappa : r[e]] \mid \mathbb{d} \rangle^{\circ} \text{ (forwarding an effect)}. $$

In either subcase, there exist $\mathbb{S}$, $\sigma'$ such that $\mathbb{J} = \langle \langle e \{\delta\} | S \circ \kappa [r\{\delta\}] | \mathbb{I} \rangle; \gamma; \Box \delta \rangle$ and $\mathbb{U} = \langle \sigma' | \eta | \phi \rangle$.

By hypothesis, we have that $\forall f \in \phi$. $\mathbf{set}(f) \subseteq \mathbf{dom}(\gamma)$ and $r \wedge \Box f$.

If $\Box= ?$, then $r$ is even-length, and by taking $\mathbb{S} = \kappa[r\{\delta\}]$, we have $\mathbb{S}\{\delta^1\} = \kappa : r$ and $\kappa : r \wedge? f$. If otherwise $\Box= !$, then $\eta = \emptyset$.

Thus in both cases, we have $\Box \delta \sim \mathbf{fwd} \eta$, and we can conclude that $\mathbf{Compatible}(\mathbb{J}, \mathbb{U})$.

$$ \mathbf{Case} \ \mathbb{I} = \langle \langle t | S \circ S | \mathbb{I} \rangle; \gamma; \delta \rangle. $$

$$ \mathbf{Subcase} \ \alpha ::= \mathbf{d.} \langle \mathbf{ret} \ \mathbb{V} \mid \Box \rangle^{\circ} \mid \mathbf{k.} \langle \Box[\mathbf{ret} \ \mathbb{V}] \mid \mathbb{c} \rangle^{\circ} \mid \mathbf{f.} \langle \Box \ \mathbb{V} \mid \mathbb{c} \rangle^{\circ} \rangle^{\circ}. $$

In either subcase, there exist $\gamma'$ and $\sigma'$ s.t. $\mathbb{J} = \langle \mathbb{I}; \gamma \cdot \gamma'; \emptyset \rangle$ and $\mathbb{U} = \langle \sigma' | \emptyset | \phi \rangle$. By defintion, we have $\emptyset \sim \mathbf{fwd} \emptyset$, and by hypothesis we have $\forall f \in \phi$. $\mathbf{set}(f) \subseteq \mathbf{dom}(\gamma)$, and in particular $\forall f \in \phi$. $\mathbf{set}(f) \subseteq \mathbf{dom}(\gamma \cdot \gamma')$, thus $\mathbf{Compatible}(\mathbb{J}, \mathbb{U})$.

$$ \mathbf{Subcase} \ \alpha ::= \mathbf{d.} \langle \kappa : r[e] \mid \Box \rangle^{\circ} \mid \kappa'. \langle \Box[\kappa : r[e]] \mid \mathbb{c} \rangle^{\circ} \rangle^{\circ}. $$

In either subcase, there exist $\gamma'$, $\sigma'$, $\eta'$, $S'$ and $\mathbb{T}$ s.t. $\mathbb{J} = \langle \mathbb{I}; \gamma' \cdot \gamma'; \Box \xi \rangle$ and $\mathbb{U} = \langle \sigma' | \eta' | \phi \rangle$, where $\mathbb{S} = \mathbb{T} \oplus S'$, $S\{\delta^{-1}\} = r$ and $\xi = (e, r, \delta \cdot [\kappa \mapsto \mathbb{T}])$.

By hypothesis, we have that $\forall f \in \phi$. $\mathbf{set}(f) \subseteq \mathbf{dom}(\gamma)$ and $r \wedge \Box f$.

If $\Box= ?$, then $r$ is odd-length and $\eta' = (f \oplus [\kappa], e)$, thus $\kappa : r \wedge? f \oplus [\kappa]$. If otherwise $\Box= !$, then $\eta = \eta' = \emptyset$.

Thus in both cases, we have $\Box \xi \sim \mathbf{fwd} \eta$, and we can conclude that $\mathbf{Compatible}(\mathbb{J}, \mathbb{U})$.

□

## D.3 Semantic ciu-observation

Given a term $\mathbb{I}; \Gamma; \emptyset \vdash_c t : \tau$, an *observer* of $t$ is an environment given by an evaluation context and a name valuation $(\mathbb{S}, v)$ such that $\mathbb{I}'; \emptyset \vdash \mathbb{S} : \tau \rightsquigarrow \mathbb{I}$ and $\mathbb{I}'; \emptyset \vdash v : \Gamma$.

We want to give a semantic characterization of "observing $\langle \cdot \rangle$" but first we need to introduce the notion of closed compossibility of OGS configurations, which is the semantic counterpart of $t$ being composable with $(\mathbb{S}, v)$ and $\mathbb{S}[t\{v\}]$ being a closed term of type 1.

### D.3.1 Closed compossibility of OGS configurations.
If complementarity guarantees the "closedness" part of closed compossibility, we still require non-intial program and environment configurations to agree on their history of interaction. We will capture this coherence of trajectory by the following synchronicity relation.

First, we will the notion of *return frame* and auxiliary definitions.

**Definition D.7** (*return frames*). We will call a *return frame* any control-flow stack of the shape $f \oplus [c]$; i.e. that it is made up of a call frame ($f \in \text{List}(\mathcal{K})$) to which is appended a single abstract undelimited continuation ($c \in \mathcal{C}$).

We will also define the function $F$ that, given an evaluation stack, computes the associated *return frame*.

$$ F(c[S]) := F(S) \oplus [c] \quad F(\mathbb{T}[\kappa[S]]) := F(S) \oplus [\kappa] \quad F(\mathbb{T}) := [] $$

**Definition D.8** (*return frames decomposition*). For any a non-empty control-flow stack $\sigma$ generated by $\mathcal{L}_{w6}$, there corresponds a natural number $k \in \mathbb{N}^*$ and $k$ *return frames* $\sigma_1, \dots, \sigma_k$ such that $\sigma = \sigma_1 \oplus \dots \oplus \sigma_k$.

We will write $\sigma_1 \oplus \dots \oplus \sigma_k$ for this unique decomposition of $\sigma$.

**Definition D.9** (*Synchronicity*). We define synchronicity as a quaternary relation $\mathcal{S} \subseteq \mathcal{A} \times \mathcal{W} \times \mathcal{A} \times \mathcal{W}$.

Let $\mathbb{I} = \langle (\mathbb{M} | \mathbb{I}); \gamma_1; \Box \delta_1 \rangle$ in $\text{Confs}_{\text{act}}$, $\mathbb{J} = \langle \gamma_2, \Box(\_, r, \_,) \rangle$ in $\text{Confs}_{\text{pas}}$ where $\mathbb{M} = \langle t | c_0[S_0] \circ \mathbb{S} \rangle$ and $\Box, \circ, \Box \in \{?, !\}$, Let $\mathbb{W} = \langle \sigma_{\mathbb{W}} | (f_{\mathbb{W}}, e_{\mathbb{W}}) | \phi_{\mathbb{W}} \rangle$, $\mathbb{U} = \langle \sigma_{\mathbb{U}} | (f_{\mathbb{U}}, e_{\mathbb{U}}) | \phi_{\mathbb{U}} \rangle$ in $\mathbb{W}$ where $\sigma_0 \oplus \dots \oplus \sigma_k$ and $\sigma'_0 \oplus \dots \oplus \sigma'_p$ (for some $k, p \in \mathbb{N}^*$) are the respective decompositions of $\sigma_{\mathbb{W}}$ and $\sigma_{\mathbb{U}}$ into *return frames*.

We say that $\langle \mathbb{I}, \mathbb{W} \rangle$ and $\langle \mathbb{J}, \mathbb{U} \rangle$ are in sync, and write $\langle \mathbb{I}, \mathbb{W} \rangle \mathcal{S} \langle \mathbb{U}, \mathbb{J} \rangle$ when the following holds:
• $I \oplus J$ and for all $i \ge 0$, we can write $\gamma_J(c_i) = d_{i+1}[S'_i]$ and $\gamma_I(d_{i+1}) = c_{i+1}[S_{i+1}]$.

• $r \wedge \blacksquare f_U$ and $r \wedge \square f_J$

• $\forall 0 \le i. F(c_i[S_i]) \approx_{\phi_U} \sigma'_i$ and $F(\gamma_J(c_i)) \approx_{\phi_W} \sigma_i$

where $\approx_{\phi}$ is given by

$$ \begin{array}{c} \text{REFL} \\ \pi = \pi' \\ \pi \approx_{\phi} \pi' \end{array} \qquad \begin{array}{c} \text{UP-TO} \\ \pi = \pi' \\ \pi \approx_{\phi} f \oplus \pi' \end{array} $$

$$ \begin{array}{c} \text{REFL} \\ \pi = \pi' \\ \pi \approx_{\phi} \pi' \end{array} \qquad \begin{array}{c} \text{UP-TO} \\ \pi = \pi' \\ \pi \approx_{\phi} f \oplus \pi' \end{array} $$

Next we show how the synchronicity relation indeed captures the coherence of both the program's and the environment's trajectories, in the sense that whatever interaction is triggered by the active player is in fact compatible with what the passive player is expecting, and that this property is preserved by interaction.

This is formalised in the next lemma, which proves that $\mathcal{S}$ is a simulation.

**LEMMA D.10 (O-SIMULATION).** Given $K \in \text{Confs}_\text{pas}$, $I \in \text{Confs}_\text{act}$, $W, U \in \mathcal{W}$ such that $\langle I, W \rangle \in \langle K, U \rangle$, we have:

$$ \begin{array}{c} \mathbb{I} \xrightarrow{m} \mathbb{J} \qquad \mathbb{W} \xrightarrow{m} w_b \qquad \mathbb{W}' \\ \exists \mathbb{J}, \mathbb{U}'. \quad \mathbb{K} \xrightarrow{m^\perp} \mathbb{J} \qquad \mathbb{U} \xrightarrow{m^\perp} w_b \qquad \mathbb{U}' \qquad \langle \mathbb{J}, \mathbb{W}' \rangle \in \langle \mathbb{J}, \mathbb{U}' \rangle \end{array} $$

**PROOF.** We write $\mathbb{I} = \langle \langle t | c_0[S_0] \circ S | I_\mathbb{I} \rangle; \gamma_\mathbb{I}, \delta_\mathbb{I} \rangle$, $\mathbb{W} = \langle \sigma_W | \eta_W | \phi_W \rangle$, $\mathbb{W}' = \langle \sigma_W' | (\cdot, r_W'), \cdot | \phi_W' \rangle$, $\mathbb{U} = \langle \sigma_\mathbb{U} | \eta_\mathbb{U} | \phi_\mathbb{U} \rangle$ and $\mathbb{K} = \langle I_\mathbb{K}; \gamma_\mathbb{K}; \xi_\mathbb{K} \rangle$. We will also write $\sigma_0 \oplus \cdots \oplus \sigma_k$ and $\sigma'_0 \oplus \cdots \oplus \sigma'_k$ (for some $k, p \in \mathbb{N}^*$) for the respective decompositions of $\sigma_W$ and $\sigma_\mathbb{U}$, as well as $\gamma_\mathbb{K}(c_i) = d_{i+1}[S'_i]$ and $\gamma_\mathbb{I}(d_{i+1}) = c_{i+1}[S_{i+1}]$ for $i \ge 0$. We proceed by case analysis on $\mathbb{m}$.

**Case m = $c_0$.** $\langle \text{ret} V | \square \rangle^\oplus$.

We have $S_0 = c_0[[]]$, $S = [[], t = \text{ret} V, \delta_\mathbb{I} = \emptyset$ and $\eta_W = \emptyset$, $r_W' = \cdot$

$\mathbb{I}, \mathbb{W} \xrightarrow{m} \langle I_\mathbb{I}; \gamma_\mathbb{I}; \emptyset \rangle, \langle \sigma_W' | \emptyset | \phi_W' \rangle$

Since $\langle \mathbb{I}, \mathbb{W} \rangle \in \langle K, U \rangle$, then $\sigma'_0 = F(c_0[[]]) = [c_0]$ and $\xi_\mathbb{K} = \emptyset$.

Thus $\mathbb{U} \xrightarrow{m^\perp} w_b \langle \sigma_\mathbb{U}' | \emptyset | \phi_\mathbb{U} \rangle = \mathbb{U}'$ and $\mathbb{K} \xrightarrow{m^\perp} \langle \langle \text{ret} V | \gamma_\mathbb{K}(c_0) | I_\mathbb{K} \rangle; \gamma_\mathbb{K}; \emptyset \rangle = \mathbb{J}$ with $\sigma_\mathbb{U}' = \sigma'_1 \oplus \cdots \oplus \sigma'_k$.

First, it is clear that $r_W' \wedge f'_U, r_W' \wedge f'_W$ and $f'_U, f'_W$ Second, by synchronicity, we have $F(\gamma_\mathbb{K}(c_l)) \approx_{\phi_W} \sigma_l$ and $F(c_l[S_l]) \approx_{\phi_U} \sigma'_l$, then if we take, for all $\ell \ge 0$, $c'_l = d_{l+1}$ and write $\gamma_\mathbb{K}(c_0) = c'_0[S'_0]$, then for all $\ell \ge 0$, we get $F(c'_l[S'_l]) \approx_{\phi_W'} \sigma_l$ and $F(\gamma_\mathbb{I}(c'_l)) \approx_{\phi_\mathbb{I}'} \sigma'_{l+1}$, i.e. $\langle \mathbb{J}, \mathbb{W}' \rangle \in \langle \mathbb{J}, \mathbb{U}' \rangle$ since $\sigma_W = \sigma_W'$ and $\sigma_\mathbb{U}' = \sigma'_1 \oplus \cdots \oplus \sigma'_k$.

**Case m = $\mathbb{K}$.** $\langle \square[\text{ret} V] | d_0 \rangle^\oplus$.

In this case, $S_0$ must be of the shape $S[\kappa[[]]], t = \text{ret} V, \xi_\mathbb{I} = \emptyset$ and $\eta_W = \emptyset$ and

$\mathbb{I}, \mathbb{W} \xrightarrow{m} \langle I_\mathbb{I}; \gamma_\mathbb{I} | d_0 \mapsto c_0[S] \rangle; \emptyset, \langle [d_0] \oplus \sigma_W | \emptyset | \phi_W \rangle$

Since $\langle \mathbb{I}, \mathbb{W} \rangle \in \langle K, U \rangle$, then $F(c_0[S[\kappa[[]]]) \approx_{\phi_\mathbb{U}} \sigma'_0$ and $\xi_\mathbb{K} = \emptyset$.

**Subcase** $F(c_0[S \circ \kappa]) = \sigma'_0$.

There exists $\sigma''_0 = F(c_0[S])$ s.t. $\sigma'_0 = \kappa \approx \sigma''_0$,

We have $\mathbb{U} \xrightarrow{m^\perp} w_b \langle \sigma''_0 \oplus \sigma'_U | \emptyset | \phi_\mathbb{U} \rangle = \mathbb{U}'$ that is

$\sigma_\mathbb{U}' = \sigma''_0 \oplus \sigma'_1 \oplus \cdots \oplus \sigma'_p$ and $\mathbb{K} \xrightarrow{m^\perp} \langle \langle \text{ret} V | d_0[\gamma_\mathbb{K}(\kappa)] | I_\mathbb{K} \rangle; \gamma_\mathbb{K}; \emptyset \rangle = \mathbb{J}$.

**Subcase** $F(c_0[S \circ \kappa]) \neq \sigma'_0$.

There exists $f \in \phi_\mathbb{U}$ s.t. $F(c_0[S \circ \kappa]) = f \oplus \sigma'_0$.

We have $\mathbb{U} \xrightarrow{m^\perp} w_b \langle \sigma''_0 \oplus \sigma'_U | \emptyset | \phi_\mathbb{U} \rangle = \mathbb{U}'$ that is $\sigma_\mathbb{U}' = \sigma''_0 \oplus \sigma'_1 \oplus \cdots \oplus \sigma'_p$ where $f = \kappa \approx f'$ and $\sigma''_0 = f' \oplus \sigma'_0$ and $\mathbb{K} \xrightarrow{m^\perp} \langle \langle \text{ret} V | d_0[\gamma_\mathbb{K}(\kappa)] | I_\mathbb{K} \rangle; \gamma_\mathbb{K}; \emptyset \rangle = \mathbb{J}$.

In either subcase, let's write $d_0[S''_0]$ for $d_0[\gamma_\mathbb{K}(\kappa)]$ and, for all $\ell \ge 0$, $S''_{\ell+1} = S'_\ell$.

First, it is clear that $r_W' \wedge f'_U, r_W' \wedge f'_W$ and that $F(d_0[S''_0]) \approx_{\phi_W'} [d_0]$ and that $F(\gamma_\mathbb{J}(d_0)) \approx_{\phi_\mathbb{J}'} \sigma''_0$, since $\phi_\mathbb{U} = \phi_\mathbb{U}'$, $\phi_W' = \phi_W''$ and $\gamma_\mathbb{J}(d_0) = \gamma_\mathbb{I}(d_0) = c_0[S]$.

Then we have, by synchronicity, for all $\ell \ge 0$, $F(\gamma_\mathbb{K}(c_l)) \approx_{\phi_W'} \sigma_l$ and $F(c_l[S_l]) \approx_{\phi_\mathbb{U}} \sigma'_l$, that is, for all $\ell \ge 1$, $F(d_l[S''_l]) \approx_{\phi_W'} \sigma_l$ and $F(\gamma_\mathbb{I}(d_l)) \approx_{\phi_\mathbb{I}'} \sigma'_l$.

Thus we can conclude that $\langle \mathbb{J}, \mathbb{W}' \rangle \in \langle \mathbb{J}, \mathbb{U}' \rangle$.

**Case m = $c_0$.** $\langle \kappa \approx r[e] | \square \rangle^\oplus$.

In this case, $\langle t | c_0[S_0] \circ S \rangle$ must be of the shape $\langle e | c_0[[]] \circ T \oplus S \rangle$, **Subcase e = $\mathbb{I}$**

$\mathbb{I}, \mathbb{W} \xrightarrow{m} \langle I_\mathbb{I}; \gamma_\mathbb{I}; ! (e, \kappa \approx r, \delta_\mathbb{I} \circ [\kappa \mapsto T]) \rangle, \langle \sigma_W | (f_W \oplus [\kappa], e) | \phi_W \rangle$.

Since $\langle \mathbb{I}, \mathbb{W} \rangle \in \langle K, U \rangle$, then $F(c_0[[]]) \approx_{\phi_\mathbb{U}} \sigma'_0$, i.e $\sigma'_0 = [c_0]$ and $\xi_\mathbb{K} = ?(e, r, \delta_\mathbb{K})$.

We have then $\mathbb{K} \xrightarrow{m^\perp} \langle \langle e | \gamma_\mathbb{K}(c_0) \circ \kappa[r\{\delta_\mathbb{K}\}] | I_\mathbb{K} \rangle; \gamma_\mathbb{K}; ?(e, \kappa \approx r, \delta_\mathbb{K}) \rangle = \mathbb{J}$ and $\mathbb{U} \xrightarrow{m^\perp} w_b \langle \sigma'_1 \oplus \cdots \oplus \sigma'_p | (f_\mathbb{U}, e) | \phi_\mathbb{U} \rangle = \mathbb{U}'$

By synchronicity, we have $F(\gamma_\mathbb{K}(c_l)) \approx_{\phi_W} \sigma_l$ and $F(c_l[S_l]) \approx_{\phi_\mathbb{U}} \sigma'_l$ and $r \wedge ?f_W$ and $r \wedge ?f_\mathbb{U}$ then if we take, for all $\ell \ge 0$, $c'_l = d_{l+1}$ and write $\gamma_\mathbb{K}(c_0) = c'_0[S'_0]$, we get $\kappa \approx r \wedge ?f_\mathbb{U}'$, $\kappa \approx r \wedge ?f_W'$ and for all $\ell \ge 0$ we get $F(c'_l[S'_l]) \approx_{\phi_W'} \sigma_l$ and $F(\gamma_\mathbb{I}(c'_l)) \approx_{\phi_\mathbb{I}'} \sigma'_{l+1}$, i.e. $\langle \mathbb{J}, \mathbb{W}' \rangle \in \langle \mathbb{J}, \mathbb{U}' \rangle$ since $\sigma_W = \sigma_W'$ and $\sigma_\mathbb{U}' = \sigma'_1 \oplus \cdots \oplus \sigma'_p$.

**Subcase e = $e$.** $\mathbb{I}, \mathbb{W} \xrightarrow{m} \langle I_\mathbb{I}; \gamma_\mathbb{I}; ?(e, \kappa \approx r, \delta_\mathbb{I} \circ [\kappa \mapsto T]) \rangle, \langle \sigma_W | (f_W \oplus [\kappa], e) | \phi_W \rangle$.

Since $\langle \mathbb{I}, \mathbb{W} \rangle \in \langle K, U \rangle$, then $F(c_0[[])) \approx_{\phi_\mathbb{U}} \sigma'_0$, i.e $\sigma'_0 = [c_0]$ and $\xi_\mathbb{K} = ! (e, r, \delta_\mathbb{K})$.

We have then $\mathbb{K} \xrightarrow{m^\perp} \langle \langle e\{\delta_\mathbb{K}\} | \gamma_\mathbb{K}(c_0) \circ \kappa[r\{\delta_\mathbb{K}\}] | I_\mathbb{K} \rangle; \gamma_\mathbb{K}; ?(e, \kappa \approx r, \delta_\mathbb{K}) \rangle = \mathbb{J}$ and $\mathbb{U} \xrightarrow{m^\perp} w_b \langle \sigma'_1 \oplus \cdots \oplus \sigma'_p | (f_\mathbb{U}, e) | \phi_\mathbb{U} \rangle = \mathbb{U}'$

By synchronicity, we have $F(\gamma_\mathbb{K}(c_l)) \approx_{\phi_W} \sigma_l$ and $F(c_l[S_l]) \approx_{\phi_\mathbb{U}} \sigma'_l$ and $r \wedge ?f_W$ and $r \wedge ?f_\mathbb{U}$ then if we take, for all $\ell \ge 0$, $c'_l = d_{l+1}$ and write $\gamma_\mathbb{K}(c_0) = c'_0[S'_0]$, we get $\kappa \approx r \wedge ?f_\mathbb{U}'$, $\kappa \approx r \wedge ?f_W'$ and for all $\ell \ge 0$ we get $F(c'_l[S'_l]) \approx_{\phi_W'} \sigma_l$ and $F(\gamma_\mathbb{I}(c'_l)) \approx_{\phi_\mathbb{I}'} \sigma'_{l+1}$, i.e. $\langle \mathbb{J}, \mathbb{W}' \rangle \in \langle \mathbb{J}, \mathbb{U}' \rangle$ since $\sigma_W = \sigma_W'$ and $\sigma_\mathbb{U}' = \sigma'_1 \oplus \cdots \oplus \sigma'_p$.

**Case m = $\mathbb{K}$.** $\langle \square[r[e]] | d_0 \rangle^\oplus$. Similar reasoning applies.

□

**COROLLARY D.11.** Given $\mathbb{J} \in \text{Confs}_\text{pas}$, $I \in \text{Confs}_\text{act}$, $\mathbb{W}, \mathbb{U} \in \mathcal{W}$ and a trace $t$ such that $\langle \mathbb{J}, \mathbb{W} \rangle \in \langle \mathbb{I}, \mathbb{U} \rangle$, $t \in \text{Tr}_{\mathcal{L}_{\mathbb{AI}}}(I)$ and $\text{Tr}_{\mathcal{L}_{\mathbb{AI}}}(\mathbb{J})$ then:

$$ t \in \text{Tr}_{\mathcal{L}_{\mathbb{W}}}(\mathbb{W}) \wedge t^\perp \in \text{Tr}_{\mathcal{L}_{\mathbb{W}}}(\mathbb{U}) $$

**PROOF.** By induction on the length of $t$ using Lemma D.10. □

**Definition D.12 (Composability).** Given a passive configuration $\mathcal{G} \in \mathcal{O}^\oplus$ and an active one $\mathcal{H} \in \mathcal{O}^\oplus$ such that $\mathcal{G} = \langle \mathbb{I} \mid \mathbb{T} \mid \mathbb{W} \rangle$ and
H = ⟨J | S | U⟩, we say that G and H are closed composable and write G⊥H when:

$$ \frac{G = \langle I \mid T \mid W \rangle \quad H = \langle J \mid S \mid U \rangle \quad \langle I, W \rangle \delta \langle J, U \rangle}{G \perp H} $$

**REMARK 4.** The preservation of closed composability by configuration synchronization follows from lemmas A.2 and D.10.

**D.3.2** OGS Observation. Now we can semantically capture S[t{v}] ⇝op⟨⟩ by the following predicate.

**Definition D.13 (Observation predicate).** Taking a passive configuration $G \in O^\Theta$ and an active one $H \in O^\oplus$ such that $G \perp H$, we define the observation of $G$ on $H$ as the predicate:

$$ \langle G \perp H \rangle \Downarrow [c] \text{ret}(\langle \rangle) \iff \exists K, \gamma. \langle J \perp I \rangle \Downarrow_{\text{ci}} \langle K \perp c[\text{ret}(\langle \rangle)]; \gamma; \perp \rangle $$

Now, that we have given a sensible notion of observation at the level of OGS configurations, it remains to show what does this predicate mean at the level of OGS interpretations.

**THEOREM D.14 (FULL OBSERVATION).** Given two composable configurations $G$ and $H$, we have:

$$ \langle H \perp G \rangle \Downarrow [c] \text{ret}(\langle \rangle) $$

if and only if

$$ \exists t \in \text{CT}_{\text{ogs}}(G), t^{\perp} \text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus} \in \text{CT}_{\text{ogs}}(H) $$

**PROOF.** We write $G = \langle I \mid T \mid W \rangle$ and $H = \langle J \mid S \mid U \rangle$ and $I = \langle (t | I); \gamma; \xi \rangle$

**Left to right.** Suppose there exist $K, J \in \mathcal{A}$ and $\gamma$ such that $\langle J \perp I \rangle \Downarrow_{\text{ci}} \langle K \perp J \rangle$ with $J = \langle (c[\text{ret}(\langle \rangle)] | I); \gamma; \emptyset \rangle$.

By corollary A.5 and definition A.3, there exists an odd-length trace $t$ such that $I \overset{t}{\Rightarrow}_I K$ and $J \overset{t^{\perp}}{\Rightarrow}_J J \underset{\text{equiv}}{\overset{\text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus}}{\Rightarrow}}_I \langle \gamma; \emptyset \rangle = J'$. By lemma D.3, there exist $T', S', S'' \in \mathcal{T}$ s.t. $T \overset{t}{\Rightarrow}_T T'$, $S \overset{t^{\perp}}{\Rightarrow}_S S' \underset{\text{equiv}}{\overset{\text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus}}{\Rightarrow}}_T S''$, $K \otimes T'$, $J' \otimes S'$ and $J' \otimes S''$. Similarly, corollary D.11 ensures the existence of $W'$, $U'$, $U'' \in \mathcal{W}$ s.t. $W \overset{t}{\Rightarrow}_{W'} W'$, $U \overset{t^{\perp}}{\Rightarrow}_{W'} U' \underset{\text{equiv}}{\overset{\text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus}}{\Rightarrow}}_{W'} U''$ whereas lemma D.10 ensures that synchronicity is preserved and that in particular $\langle J, U' \rangle \delta \langle K, W' \rangle$.

Thus we have shown that $G \underset{\text{ogs}}{\overset{t}{\Rightarrow}} \langle K \mid T' \mid W' \rangle$ and

$$ H \underset{\text{ogs}}{\overset{t^{\perp}}{\Rightarrow}} \langle J \mid S' \mid U' \rangle \underset{\text{ogs}}{\overset{\text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus}}{\Rightarrow}} \langle J' \mid S'' \mid U'' \rangle, $$
from which we can deduce that $t \in \text{Tr}_{\text{ogs}}(G)$ and $t^{\perp} \text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus} \in \text{Tr}_{\text{ogs}}(H)$.

**Right to left.** Let $t \in \text{Tr}_{\text{ogs}}$ such that $t \in \text{Tr}_{\text{ogs}}(G)$ and $t^{\perp} \text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus} \in \text{Tr}_{\text{ogs}}(H)$.

If we write $G \underset{\text{ogs}}{\overset{t}{\Rightarrow}} \langle K \mid T' \mid W' \rangle$ and for some $W' \in \mathcal{W}$

with $K = \langle I_K; \gamma_K; \emptyset \rangle \in \mathcal{A}$, and write $H \underset{\text{ogs}}{\overset{t^{\perp}}{\Rightarrow}} \langle J \mid S' \mid U' \rangle \underset{\text{equiv}}{\overset{\text{c.} \langle \text{ret}(\langle \rangle) | \Box \rangle^{\oplus}}{\Rightarrow}}_{\text{ogs}} \mathbb{B}$ for some $S' \in \mathcal{T}$, $U' \in \mathcal{W}$ and $\mathbb{B} \in \mathcal{O}$ with $J = \langle (c[\text{ret}(\langle \rangle)] | I); \gamma; \emptyset \rangle$, then by corollary A.5, we have $\langle J \perp I \rangle \mapsto_{\text{ci}}^* \langle J \perp K \rangle$ and again by lemma A.2, we have $J \perp_c K$, and in particular $c \notin \text{dom}(\gamma_J)$, thus $\langle J \perp K \rangle \mapsto_{\text{ci}}^*$.

Finally, we have shown that $\langle J \perp I \rangle \Downarrow_{\text{ci}} \langle J \perp K \rangle$ and consequently $\langle H \perp G \rangle \Downarrow [c] \text{ret}(\langle \rangle)$. □