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

HAL
open science

# Leaf-First Zipper Semantics

Sergueï Lenglet, Alan Schmitt

► To cite this version:

Sergueï Lenglet, Alan Schmitt. Leaf-First Zipper Semantics. 2024. hal-04537440

HAL Id: hal-04537440

https://inria.hal.science/hal-04537440

Preprint submitted on 9 Apr 2024

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Leaf-First Zipper Semantics

Sergueï Lenglet¹² and Alan Schmitt³

¹ Université de Lorraine, Nancy, France

² Université Sorbonne Paris Nord, Villetaneuse, France

³ INRIA, Rennes, France

**Abstract.** Biernacka et al. recently proposed *zipper semantics*, a semantics format from which sound and complete abstract machines for non-deterministic languages can be automatically derived. We present a new style of zipper semantics, called *leaf-first*, in which we express the semantics of two extensions of $HO_π$, a higher-order version of the $π$-calculus: one with passivation and the other with join patterns. The leaf-first style is better suited than the original one to express phenomena occurring in process calculi semantics such as scope extrusion, which is observable with passivation and complex with join patterns.

**Keywords:** Process calculi · Abstract machines · Scope extrusion.

## 1 Introduction

In concurrency theory, abstract machines are used as an implementation model [9, 11, 18, 20, 26], in particular to study the distribution of computation [1, 12–14, 16, 21]. The design of these machines is often ad-hoc, following principles which apply to the considered calculus only. Besides, some of the machines are not complete, i.e., there exist reduction paths of the language which cannot be simulated by its abstract machine [9, 11, 13, 18, 26]. To overcome these issues, Biernacka et al. [2, 3] recently proposed Non-Deterministic Abstract Machines (NDAM), a generic design of abstract machines for non-deterministic languages. An NDAM explores the term in the search for a redex, making arbitrary choices when several paths are possible. The machine backtracks when it reaches a normal form, annotating it to not try it again, thus avoiding infinite loops during the search.

As writing the definition of an NDAM can be tedious, the authors also propose a sound and complete automatic derivation procedure from a *zipper semantics*, a format in between a Structural Operational Semantics (SOS) [22] and a context-based reduction semantics [7, 8]. Like in a SOS, a zipper semantics explores a term with structural rules, but it remembers its position in the term using an evaluation context, a syntactic object that represents a term with a hole [8]. A zipper semantics respecting some properties can then be augmented into an NDAM by adding the annotations and backtracking mechanisms.

Biernacka et al. [2] define a zipper semantics for several calculi including $HO_π$ [23], a process calculus where messages are executable terms. Like the $π$-calculus [24], $HO_π$ features name restriction, a construct which restricts the
# Leaf-First Zipper Semantics

Sergueï Lenglet¹² and Alan Schmitt³

¹ Université de Lorraine, Nancy, France

² Université Sorbonne Paris Nord, Villetaneuse, France

³ INRIA, Rennes, France

**Abstract.** Biernacka et al. recently proposed *zipper semantics*, a semantics format from which sound and complete abstract machines for non-deterministic languages can be automatically derived. We present a new style of zipper semantics, called *leaf-first*, in which we express the semantics of two extensions of $HO_π$, a higher-order version of the $π$-calculus: one with passivation and the other with join patterns. The leaf-first style is better suited than the original one to express phenomena occurring in process calculi semantics such as scope extrusion, which is observable with passivation and complex with join patterns.

**Keywords:** Process calculi · Abstract machines · Scope extrusion.

## 1 Introduction

In concurrency theory, abstract machines are used as an implementation model [9, 11, 18, 20, 26], in particular to study the distribution of computation [1, 12–14, 16, 21]. The design of these machines is often ad-hoc, following principles which apply to the considered calculus only. Besides, some of the machines are not complete, i.e., there exist reduction paths of the language which cannot be simulated by its abstract machine [9, 11, 13, 18, 26]. To overcome these issues, Biernacka et al. [2, 3] recently proposed Non-Deterministic Abstract Machines (NDAM), a generic design of abstract machines for non-deterministic languages. An NDAM explores the term in the search for a redex, making arbitrary choices when several paths are possible. The machine backtracks when it reaches a normal form, annotating it to not try it again, thus avoiding infinite loops during the search.

As writing the definition of an NDAM can be tedious, the authors also propose a sound and complete automatic derivation procedure from a *zipper semantics*, a format in between a Structural Operational Semantics (SOS) [22] and a context-based reduction semantics [7, 8]. Like in a SOS, a zipper semantics explores a term with structural rules, but it remembers its position in the term using an evaluation context, a syntactic object that represents a term with a hole [8]. A zipper semantics respecting some properties can then be augmented into an NDAM by adding the annotations and backtracking mechanisms.

Biernacka et al. [2] define a zipper semantics for several calculi including $HO_π$ [23], a process calculus where messages are executable terms. Like the $π$-calculus [24], $HO_π$ features name restriction, a construct which restricts the
scope of a communication channel, hiding it to the outside. When a communication happens between a sender and a receiver, it may be necessary to enlarge the scope of restricted names to include the receiver: this phenomenon is known as *scope extrusion*. Biernacka et al. consider a variant of HOπ with *eager* scope extrusion, where the scope of all name restrictions around the message output are extended to include the input. In contrast, in *lazy* scope extrusion, only the restrictions of the names occurring in the message contents are extended.

While the difference between lazy and eager scope extrusion cannot be observed in HOπ, it may lead to distinguishable behaviors in calculi with localities and *passivation* [1, 17], a feature used in component models to interrupt and capture the state of running components [25]. Lazy scope extrusion is also quite intricate in presence of *join patterns* [11], where a single receiver may receive messages from different senders at once. The scope of lazily extruded names should encompass the process sending the message and the receiver, and no more. With several messages emitted at once, the scopes of names restricting two distinct messages are different and depend on the respective output processes.

In this paper, we encode lazy scope extrusion in various settings by defining a new format of zipper semantics, called *leaf-first*. Our contributions are: we express the semantics of HOπ with passivation and lazy scope extrusion in our new leaf-first format, and we show that our approach can also handle an extension of HOπ with join patterns. Our format respects the zipper semantics requirements, so we can apply Biernacka et al.'s derivation procedure to obtain an NDAM from it, and we get for free abstract machines for these calculi.

The paper is organized as follows. Section 2 presents the syntax and lazy semantics of HOπ with passivation; we recall an example illustrating how we can distinguish lazy from eager scope extrusion in that calculus. We then present a leaf-first zipper semantics for this calculus, that we prove equivalent to the usual one. Section 3 follows the same structure for HOπ with join patterns. Section 4 discusses related work and concludes. The appendix contains the missing proofs.

# 2 HOπ with Passivation

We present the lazy semantics of HOπP (HOπ with passivation) [17], that we characterize using the new zipper semantics style we propose in this paper.

## 2.1 Syntax and Lazy Semantics

*Syntax.* HOπP [17] is a higher-order calculus—where messages are executable processes—extended with hierarchical localities and passivation. We assume countable sets of channel names, ranged over by lowercase letters *a*, *b*, etc, and of process variables ranged over by *X*, *Y*, *Z*. The syntax of processes is as follows.

$$ P, Q, R, S, M, K ::= X \mid \mathbf{0} \mid P \parallel Q \mid a(X).R \mid \bar{a}\langle M \rangle K \mid \nu a.P \mid a[P] $$

Informally, **0** is the inactive process, the parallel composition $P \parallel Q$ is executing *P* and *Q* concurrently, $\nu a.P$ restricts the scope of channel *a* to *P*, an output
scope of a communication channel, hiding it to the outside. When a communication happens between a sender and a receiver, it may be necessary to enlarge the scope of restricted names to include the receiver: this phenomenon is known as *scope extrusion*. Biernacka et al. consider a variant of HOπ with *eager* scope extrusion, where the scope of all name restrictions around the message output are extended to include the input. In contrast, in *lazy* scope extrusion, only the restrictions of the names occurring in the message contents are extended.

While the difference between lazy and eager scope extrusion cannot be observed in HOπ, it may lead to distinguishable behaviors in calculi with localities and *passivation* [1, 17], a feature used in component models to interrupt and capture the state of running components [25]. Lazy scope extrusion is also quite intricate in presence of *join patterns* [11], where a single receiver may receive messages from different senders at once. The scope of lazily extruded names should encompass the process sending the message and the receiver, and no more. With several messages emitted at once, the scopes of names restricting two distinct messages are different and depend on the respective output processes.

In this paper, we encode lazy scope extrusion in various settings by defining a new format of zipper semantics, called *leaf-first*. Our contributions are: we express the semantics of HOπ with passivation and lazy scope extrusion in our new leaf-first format, and we show that our approach can also handle an extension of HOπ with join patterns. Our format respects the zipper semantics requirements, so we can apply Biernacka et al.'s derivation procedure to obtain an NDAM from it, and we get for free abstract machines for these calculi.

The paper is organized as follows. Section 2 presents the syntax and lazy semantics of HOπ with passivation; we recall an example illustrating how we can distinguish lazy from eager scope extrusion in that calculus. We then present a leaf-first zipper semantics for this calculus, that we prove equivalent to the usual one. Section 3 follows the same structure for HOπ with join patterns. Section 4 discusses related work and concludes. The appendix contains the missing proofs.

## 2 HOπ with Passivation

We present the lazy semantics of HOπP (HOπ with passivation) [17], that we characterize using the new zipper semantics style we propose in this paper.

### 2.1 Syntax and Lazy Semantics

*Syntax.* HOπP [17] is a higher-order calculus—where messages are executable processes—extended with hierarchical localities and passivation. We assume countable sets of channel names, ranged over by lowercase letters *a*, *b*, etc, and of process variables ranged over by *X*, *Y*, *Z*. The syntax of processes is as follows.

$$ P, Q, R, S, M, K ::= X \mid \mathbf{0} \mid P \parallel Q \mid a(X).R \mid \bar{a}\langle M \rangle K \mid \nu a.P \mid a[P] $$

Informally, **0** is the inactive process, the parallel composition $P \parallel Q$ is executing *P* and *Q* concurrently, $\nu a.P$ restricts the scope of channel *a* to *P*, an output
$\bar{a}\langle M \rangle K$ is sending $M$ on $a$ and continues as $K$, while $a(X).R$ is waiting for a message $M$ on $a$ to continue as $R$ where $X$ is replaced by $M$. A process may run in a locality $a[P]$, which can be passivated (dissolved) at any time, interrupting the execution of $P$ and saving its current state in a message on $a$.

For readability, we often use $S$ to denote a sending process, $R$ a receiving one, $M$ a message, and $K$ a continuation, but these all stand for processes. In examples, we also often omit $0$ in output continuations or in parallel processes, abbreviating $\bar{a}\langle P \rangle 0$ as $\bar{a}\langle P \rangle$ and $P \parallel 0$ as $P$. The scope of name restriction extends to the right as much as possible, writing $\nu a.(P \parallel Q)$ as $\nu a.P \parallel Q$.

**Scope extrusion.** The scope of $a$ in $\nu a.P$ is restricted to $P$, so that a communication on $a$ is possible inside $P$ only. It does not prevent communication on other names, but the scope of restricted names present in a message has to be enlarged to prevent them from escaping their binder. For example, we have

$$b(X).(X \parallel \bar{c}\langle 0 \rangle) \parallel \nu a.d.\bar{b}\langle \bar{a}\langle 0 \rangle \rangle \parallel \bar{d}\langle 0 \rangle \xrightarrow{\tau} \nu a.\bar{a}\langle 0 \rangle \parallel \bar{c}\langle 0 \rangle \parallel \nu d.\bar{d}\langle 0 \rangle$$

The scope of $a$ is extended to include the receiver, a phenomenon known as *scope extrusion*. The scope of $d$, however, remains the same: we only extend the scope of names occurring in the message. The scope extrusion is thus said to be *lazy*.

In $\nu a.P$, $a$ is bound in $P$, and $a(X).R$ binds $X$ in $R$. We write $\text{fn}(P)$ for free names of $P$, defined as expected. To avoid unwanted captures (in particular during scope extrusion), we henceforth assume bound names and variables to be pairwise distinct, and distinct from the free names and variables of all the processes under consideration, using $\alpha$-conversion if necessary. This convention matters for instance for the rules `OUTPAR`, `OUTLOC`, and `TAUCom` of Figure 1.

**Lazy semantics.** Given an entity ranged over by $e$, we write $\vec{e}$ for a sequence $(e_1...e_n)$. We write $\langle \rangle$ for the empty sequence, $e' \cdot \vec{e}$ for the extension of a sequence to the left, and $\vec{e_1} \cdot \vec{e_2}$ for the concatenation of two sequences. We write $P\{Q/X\}$ for the usual capture-avoiding substitution of $X$ by $Q$ in $P$.

We define the labeled operational semantics with three judgments: $P \xrightarrow{\tau} P'$ for silent steps, $P \xrightarrow{a(M)} R$ for a process that inputs the message $M$ on $a$, and $P \xrightarrow{\nu \vec{b}.\bar{a}\langle M \rangle} K$ for a process that outputs the message $\bar{a}\langle M \rangle$ while extruding the names in $\vec{b}$. We give the rules in Figure 1, except the symmetric counterpart of the rules marked with $(s)$, a convention we follow from now on.

A transition $P \xrightarrow{\tau} P'$ can be decomposed as follows. First, we apply the rules `TAUPAR`, `TAULOC`, and `TAUNU` to reach the parallel composition of the communication. At this point, rule `TAUCom` is applied, with two premises. In one premise, output rules `OUTPAR`, `OUTLOC`, `OUTEXTR`, and `OUTNU` are applied until the messaging process. The last two rules are for name restriction, the former is used when the name needs to be extruded (it is free in the message contents), while the latter is used when no extrusion is needed. The message may be the result of an output (rule `OUTOUT`) or a passivation (rule `OUTPASSIV`). In the other premise of the `TAUCom` rule, the input is reached through rules
$\bar{a}\langle M \rangle K$ is sending $M$ on $a$ and continues as $K$, while $a(X).R$ is waiting for a message $M$ on $a$ to continue as $R$ where $X$ is replaced by $M$. A process may run in a locality $a[P]$, which can be passivated (dissolved) at any time, interrupting the execution of $P$ and saving its current state in a message on $a$.

For readability, we often use $S$ to denote a sending process, $R$ a receiving one, $M$ a message, and $K$ a continuation, but these all stand for processes. In examples, we also often omit $0$ in output continuations or in parallel processes, abbreviating $\bar{a}\langle P \rangle 0$ as $\bar{a}\langle P \rangle$ and $P \parallel 0$ as $P$. The scope of name restriction extends to the right as much as possible, writing $\nu a.(P \parallel Q)$ as $\nu a.P \parallel Q$.

**Scope extrusion.** The scope of $a$ in $\nu a.P$ is restricted to $P$, so that a communication on $a$ is possible inside $P$ only. It does not prevent communication on other names, but the scope of restricted names present in a message has to be enlarged to prevent them from escaping their binder. For example, we have

$$b(X).(X \parallel \bar{c}\langle 0 \rangle) \parallel \nu a.d.\bar{b}\langle \bar{a}\langle 0 \rangle \rangle \parallel \bar{d}\langle 0 \rangle \xrightarrow{\tau} \nu a.\bar{a}\langle 0 \rangle \parallel \bar{c}\langle 0 \rangle \parallel \nu d.\bar{d}\langle 0 \rangle$$

The scope of $a$ is extended to include the receiver, a phenomenon known as *scope extrusion*. The scope of $d$, however, remains the same: we only extend the scope of names occurring in the message. The scope extrusion is thus said to be *lazy*.

In $\nu a.P$, $a$ is bound in $P$, and $a(X).R$ binds $X$ in $R$. We write $\text{fn}(P)$ for free names of $P$, defined as expected. To avoid unwanted captures (in particular during scope extrusion), we henceforth assume bound names and variables to be pairwise distinct, and distinct from the free names and variables of all the processes under consideration, using $\alpha$-conversion if necessary. This convention matters for instance for the rules `OUTPAR`, `OUTLOC`, and `TAUCom` of Figure 1.

**Lazy semantics.** Given an entity ranged over by $e$, we write $\vec{e}$ for a sequence $(e_1...e_n)$. We write $()$ for the empty sequence, $e' \cdot \vec{e}$ for the extension of a sequence to the left, and $\vec{e_1} \cdot \vec{e_2}$ for the concatenation of two sequences. We write $P\{Q/X\}$ for the usual capture-avoiding substitution of $X$ by $Q$ in $P$.

We define the labeled operational semantics with three judgments: $P \xrightarrow{\tau} P'$ for silent steps, $P \xrightarrow{a(M)} R$ for a process that inputs the message $M$ on $a$, and $P \xrightarrow{\nu \vec{b}.\bar{a}\langle M \rangle} K$ for a process that outputs the message $\bar{a}\langle M \rangle$ while extruding the names in $\vec{b}$. We give the rules in Figure 1, except the symmetric counterpart of the rules marked with $(s)$, a convention we follow from now on.

A transition $P \xrightarrow{\tau} P'$ can be decomposed as follows. First, we apply the rules `TAUPAR`, `TAULOC`, and `TAUNU` to reach the parallel composition of the communication. At this point, rule `TAUCom` is applied, with two premises. In one premise, output rules `OUTPAR`, `OUTLOC`, `OUTEXTR`, and `OUTNU` are applied until the messaging process. The last two rules are for name restriction, the former is used when the name needs to be extruded (it is free in the message contents), while the latter is used when no extrusion is needed. The message may be the result of an output (rule `OUTOUT`) or a passivation (rule `OUTPASSIV`). In the other premise of the `TAUCom` rule, the input is reached through rules
<figure><img src="image_1.png" /><figcaption>Fig. 1. Lazy Semantics of HOπP</figcaption></figure>

INPAR, INLOC, and INNU, and the actual input is done in rule ININ. Finally, the
conclusion of TAUCom restores the name restrictions that have been extruded.

Example. We show the difference between lazy and eager scope extrusion in
a calculus with passivation. We write $a(X).P$ as $a(-).P$ if $X$ is not free in $P$.
Let $P = a[\nu c.\bar{b}\langle 0 \rangle \bar{c}\langle 0 \rangle] \parallel c(-).c(-).\bar{d}\langle 0 \rangle] \parallel b(-).a(X).X \parallel X$. We communicate on $b$
and then passivate the locality on $a$, duplicating its content. With eager scope
extrusion, the scope of $c$ is expanded outside $a$:

$$
\begin{align*}
& P \xrightarrow{\tau} \nu c. a[\bar{c}\langle 0 \rangle] \parallel c(-).c(-).\bar{d}\langle 0 \rangle] \parallel a(X).(X \parallel X) \\
& \xrightarrow{\tau} \nu c. \bar{c}\langle 0 \rangle] \parallel c(-).c(-).\bar{d}\langle 0 \rangle] \parallel \bar{c}\langle 0 \rangle] \parallel c(-).c(-).\bar{d}\langle 0 \rangle
\end{align*}
$$

The name *c* is then shared between the copies of the duplicated process, and
a message output on *d* becomes possible after two communications on *c*. With
lazy scope extrusion, the scope of *c* does not change:

$$
\begin{align*}
& P \xrightarrow{\tau} a[\nu c. \bar{c}\langle 0 \rangle] \parallel c(-).c(-).\bar{d}\langle 0 \rangle] \parallel a(X).X \parallel X \\
& \xrightarrow{\tau} \nu c.(\bar{c}\langle 0 \rangle) \parallel c(-).c(-).\bar{d}\langle 0 \rangle) \parallel \nu c.(\bar{c}\langle 0 \rangle) \parallel c(-).c(-).\bar{d}\langle 0 \rangle)
\end{align*}
$$

Each duplicated process has its own copy of *c*, and it is no longer possible for
the message output on *d* to trigger.
<figure><img src="image_3.png" /><figcaption>Fig. 1. Lazy Semantics of HOπP</figcaption></figure>

INPAR, INLOC, and INNU, and the actual input is done in rule ININ. Finally, the
conclusion of TAUCom restores the name restrictions that have been extruded.

Example. We show the difference between lazy and eager scope extrusion in
a calculus with passivation. We write $a(X).P$ as $a(-).P$ if $X$ is not free in $P$.
Let $P = a[\nu c.\bar{b}\langle\mathbf{0}\rangle\bar{c}\langle\mathbf{0}\rangle] \parallel c(-).c(-).\bar{d}\langle\mathbf{0}\rangle] \parallel b(-).a(X).X \parallel X$. We communicate on $b$
and then passivate the locality on $a$, duplicating its content. With eager scope
extrusion, the scope of $c$ is expanded outside $a$:

$$
\begin{align*}
& P \xrightarrow{\tau} \nu c. a[\bar{c}\langle\mathbf{0}\rangle] \parallel c(-).c(-).\bar{d}\langle\mathbf{0}\rangle] \parallel a(X).(X \parallel X) \\
& \xrightarrow{\tau} \nu c. \bar{c}\langle\mathbf{0}\rangle] \parallel c(-).c(-).\bar{d}\langle\mathbf{0}\rangle] \parallel \bar{c}\langle\mathbf{0}\rangle] \parallel c(-).c(-).\bar{d}\langle\mathbf{0}\rangle
\end{align*}
$$

The name *c* is then shared between the copies of the duplicated process, and
a message output on *d* becomes possible after two communications on *c*. With
lazy scope extrusion, the scope of *c* does not change:

$$
\begin{align*}
& P \xrightarrow{\tau} a[\nu c. \bar{c}\langle\mathbf{0}\rangle] \parallel c(-).c(-).\bar{d}\langle\mathbf{0}\rangle] \parallel a(X).X \parallel X \\
& \xrightarrow{\tau} \nu c.(\bar{c}\langle\mathbf{0}\rangle) \parallel c(-).c(-).\bar{d}\langle\mathbf{0}\rangle) \parallel \nu c.(\bar{c}\langle\mathbf{0}\rangle) \parallel c(-).c(-).\bar{d}\langle\mathbf{0}\rangle)
\end{align*}
$$

Each duplicated process has its own copy of *c*, and it is no longer possible for
the message output on *d* to trigger.
## 2.2 Root-First Zipper Semantics

Zipper semantics exhibits the step-by-step decomposition of a term into a context and a redex. Like a SOS [22], it traverses a term in the search for a redex using structural rules. It also makes explicit the current position in the term using an evaluation context, like in context-based reduction semantics [8]. We represent a context as a stack of elementary contexts $\mathfrak{F}$, called *frames*, of four kinds.

$$ \mathbb{E}, \mathbb{F}, \mathbb{G}, \mathbb{H} ::= \bullet | \mathfrak{F} ::= \mathbb{E} \qquad \mathfrak{F} ::= \|P \mid P\| \mid \nu a \mid a[\mathbb{P}] $$

Each frame corresponds to a set of similar structural rules in the definition of the lazy semantics. The decomposition process happening in a zipper semantics makes it more convenient to interpret a context inside-out: the topmost frame is the innermost one in the term. We define the operation of plugging $P$ inside a frame $\mathfrak{F}[\mathbb{P}]$ and inside a context $\mathbb{E}[\mathbb{P}]$ as follows.

$$ \bullet[\mathbb{P}] \stackrel{\Delta}{=} P \qquad (\mathfrak{F}::=\mathbb{E})[\mathbb{P}] \stackrel{\Delta}{=} \mathbb{E}[\mathfrak{F}[\mathbb{P}]] \\ (\|Q\|)[\mathbb{P}] \stackrel{\Delta}{=} P \|Q\| \qquad (Q\|\|)[\mathbb{P}] \stackrel{\Delta}{=} Q \|P\| \qquad (\nu a)[\mathbb{P}] \stackrel{\Delta}{=} \nu a.P \qquad (a\|\|)[\mathbb{P}] \stackrel{\Delta}{=} a[\mathbb{P}] $$

We use contexts to indicate where the current focus is when exploring a term: for instance, $\mathbb{E}[\mathbb{P} \| Q]$ means that the current focus is on the parallel composition. To focus on $P$, we consider $(\|Q::\mathbb{E})[\mathbb{P}]$: going further down the term consists in pushing a frame on top of the context. In contrast, going towards the root amounts to popping the top frame from the context.

In most semantics of process calculi based on labeled transitions, an input $a(X).R$ communicates with an output $\bar{a}\langle M \rangle K$ even if they are not directly in parallel. The zipper semantics therefore aims at decomposing a term as a redex in some evaluation context $\mathbb{E}$, the redex itself being of the form $\mathbb{F}[\mathbb{S}] \parallel \mathbb{G}[a(X).R]$ or $\mathbb{G}[a(X).R] \parallel \mathbb{F}[\mathbb{S}]$ with $S = \bar{a}\langle M \rangle K$ or $S = a[M]$. The strategy followed by Biernacka et al. [2, Appendix C] to decompose a $\text{HO}_\pi$ process $P$ proceeds in three steps: starting from the top of $P$, search for the parallel composition of the communication, building $\mathbb{E}$ at the same time. At that point, $P$ is decomposed as $\mathbb{E}[P_1 \parallel P_2]$. Then, look for the output in either $P_1$ or $P_2$, decomposing it as $\mathbb{F}[\bar{a}\langle M \rangle K]$. At the same time, $\mathbb{F}$ is split into $\mathbb{F}_\parallel$ and $\mathbb{F}_\nu$, so that $\mathbb{F}_\parallel$ contains the parallel compositions and $\mathbb{F}_\nu$ the name restrictions of $\mathbb{F}$. Finally, look for the input in the other process, decomposing it as $\mathbb{G}[a(X).R]$. Once all the ingredients have been found, the result of the communication is either $\mathbb{E}[\mathbb{F}_\nu[\mathbb{F}_\parallel[\mathbb{K}] \parallel \mathbb{G}[R\{Q/X\}]]]$ or $\mathbb{E}[\mathbb{F}_\nu[\mathbb{G}[R\{Q/X\}] \parallel \mathbb{F}_\parallel[\mathbb{K}]]]$. We refer to such an exploration strategy as *root-first*, because it starts the decomposition with the operator at the root of the redex (the parallel composition).

In the final result, the scope extrusion is *eager* because $\mathbb{F}_\nu$ collects all the enclosing name restrictions of $\mathbb{F}$, not only those restricting the free names of $M$. The problem is that the decomposition of $\mathbb{F}$ happens while going through the sending process, while the message $M$ is not yet known: when we reach it, the decomposition of $\mathbb{F}$ is already over. Therefore, while a root-first strategy is enough to express the $\lambda$-calculus or a process calculus with *eager* scope extrusion, it is not fit to represent the semantics of a calculus with *lazy* scope extrusion.
## 2.2 Root-First Zipper Semantics

Zipper semantics exhibits the step-by-step decomposition of a term into a context and a redex. Like a SOS [22], it traverses a term in the search for a redex using structural rules. It also makes explicit the current position in the term using an evaluation context, like in context-based reduction semantics [8]. We represent a context as a stack of elementary contexts $\mathfrak{F}$, called *frames*, of four kinds.

$$ \mathbb{E}, \mathbb{F}, \mathbb{G}, \mathbb{H} ::= \bullet | \mathfrak{F} ::= \mathbb{E} \qquad \mathfrak{F} ::= \|P \mid P\| \mid \nu a \mid a[\mathbb{P}] $$

Each frame corresponds to a set of similar structural rules in the definition of the lazy semantics. The decomposition process happening in a zipper semantics makes it more convenient to interpret a context *inside-out*: the topmost frame is the innermost one in the term. We define the operation of plugging $P$ inside a frame $\mathfrak{F}[P]$ and inside a context $\mathbb{E}[P]$ as follows.

$$ \bullet[\mathbb{P}] \stackrel{\Delta}{=} P \qquad (\mathfrak{F}::=\mathbb{E})[\mathbb{P}] \stackrel{\Delta}{=} \mathbb{E}[\mathfrak{F}[\mathbb{P}]] \\ (\|Q\|)[\mathbb{P}] \stackrel{\Delta}{=} P \|Q\| \qquad (Q\|\|)[\mathbb{P}] \stackrel{\Delta}{=} Q \|P\| \qquad (\nu a)[\mathbb{P}] \stackrel{\Delta}{=} \nu a.P \qquad (a\|\|)[\mathbb{P}] \stackrel{\Delta}{=} a[P] $$

We use contexts to indicate where the current focus is when exploring a term: for instance, $\mathbb{E}[P \| Q]$ means that the current focus is on the parallel composition. To focus on $P$, we consider $(\|Q::\mathbb{E})[P]$; going further down the term consists in pushing a frame on top of the context. In contrast, going towards the root amounts to popping the top frame from the context.

In most semantics of process calculi based on labeled transitions, an input $a(X).R$ communicates with an output $\bar{a}\langle M \rangle K$ even if they are not directly in parallel. The zipper semantics therefore aims at decomposing a term as a redex in some evaluation context $\mathbb{E}$, the redex itself being of the form $F[S] \parallel G[a(X).R]$ or $G[a(X).R] \parallel F[S]$ with $S = \bar{a}\langle M \rangle K$ or $S = a[M]$. The strategy followed by Biernacka et al. [2, Appendix C] to decompose a $\text{HO}_\pi$ process $P$ proceeds in three steps: starting from the top of $P$, search for the parallel composition of the communication, building $\mathbb{E}$ at the same time. At that point, $P$ is decomposed as $\mathbb{E}[P_1 \| P_2]$. Then, look for the output in either $P_1$ or $P_2$, decomposing it as $F[\bar{a}\langle M \rangle K]$. At the same time, $F$ is split into $F_\|$ and $F_\nu$, so that $F_\|$ contains the parallel compositions and $F_\nu$ the name restrictions of $F$. Finally, look for the input in the other process, decomposing it as $G[a(X).R]$. Once all the ingredients have been found, the result of the communication is either $\mathbb{E}[F_\nu [F_\| [K] \parallel G[R\{Q/X\}]]]$ or $\mathbb{E}[F_\nu [G[R\{Q/X\}] \parallel F_\| [K]]]$. We refer to such an exploration strategy as *root-first*, because it starts the decomposition with the operator at the root of the redex (the parallel composition).

In the final result, the scope extrusion is *eager* because $F_\nu$ collects all the enclosing name restrictions of $F$, not only those restricting the free names of $M$. The problem is that the decomposition of $F$ happens while going through the sending process, while the message $M$ is not yet known: when we reach it, the decomposition of $F$ is already over. Therefore, while a root-first strategy is enough to express the $\lambda$-calculus or a process calculus with *eager* scope extrusion, it is not fit to represent the semantics of a calculus with *lazy* scope extrusion.
<figure><img src="image_2.png" /><figcaption>Fig. 2. Leaf-First Zipper semantics for lazy HO_πP</figcaption></figure>

## 2.3 Leaf-First Zipper Semantics

As said before, finding the extruded names in $F[\overline{\langle a \rangle M} K]$ requires us to know $M$ when going through $F$. We therefore search for the output first, then for the parallel composition and the input. Because the output is a leaf of the redex, we refer to such a strategy as a *leaf-first* zipper semantics. It is defined in Figure 2.

A zipper transition $P \to_{zs} P'$ is defined using three auxiliary transitions (or modes) out, par, and in. The out mode looks for a message either from an output or a passivation. The rule init starts the search at the top of the term. The rules outParL, outParR, outLoc, and outNu change the current focus to a subterm. When we apply the rule outOut or outPassiv, the initial term is decomposed as $E[\overline{\langle a \rangle M} K]$ or $E[a[P]]$, and we switch to the par mode.

The par mode searches the parallel composition which separates the output and input processes, computing on the way the extruded names. The transition
<figure><img src="image_4.png" /><figcaption>Fig. 2. Leaf-First Zipper semantics for lazy HO_πP</figcaption></figure>

## 2.3 Leaf-First Zipper Semantics

As said before, finding the extruded names in $F[\overline{\langle a \rangle M} K]$ requires us to know $M$ when going through $F$. We therefore search for the output first, then for the parallel composition and the input. Because the output is a leaf of the redex, we refer to such a strategy as a *leaf-first* zipper semantics. It is defined in Figure 2.

A zipper transition $P \to_{zs} P'$ is defined using three auxiliary transitions (or modes) out, par, and in. The out mode looks for a message either from an output or a passivation. The rule init starts the search at the top of the term. The rules outParL, outParR, outLoc, and outNu change the current focus to a subterm. When we apply the rule outOut or outPassiv, the initial term is decomposed as $E[\overline{\langle a \rangle M} K]$ or $E[a[P]]$, and we switch to the par mode.

The par mode searches the parallel composition which separates the output and input processes, computing on the way the extruded names. The transition
$\mathbb{E} \xrightarrow{K, \vec{b}, a, M} \mathit{par} P'$ goes through $\mathbb{E}$ looking for the parallel composition, constructing $K$ (the continuation of the output) and $\vec{b}$ (the extruded names) while doing so, and remembering that $M$ is sent on $a$. The rules $\mathit{outOut}$ and $\mathit{outPassiv}$ initialize the par mode with the proper continuation and with an empty sequence of extruded names. If the context is of the form $\nu c::\mathbb{E}$, the name restriction $\nu c$ surrounds the message output, so we should check that it does not prevent the communication on $a$, hence the premise $c \neq a$ in rules $\mathit{parNu}$ and $\mathit{parExtr}$. If $c$ occurs free in the message $M$, it must be extruded, and it is added to the sequence $\vec{b}$ in the rule $\mathit{parExtr}$. Otherwise, it is added to $K$ in the rule $\mathit{parNu}$.

A locality is moved from the context to the continuation (rule $\mathit{parLoc}$). If the context is of the shape $\|Q::\mathbb{E}$ or $Q::\mathbb{E}$, we consider a process of the form $\mathbb{E}[K \| Q]$ or $\mathbb{E}[Q \| K]$ and we have two possibilities. If $Q$ is not the process receiving the message, then $Q$ has to be added to the continuation, and we continue searching for the receiver in $\mathbb{E}$ (rules $\mathit{parL}$ and $\mathit{parR}$). Otherwise, we have found the parallel composition where the communication takes place, which is where the extruded names $\vec{b}$ should be restricted. We remember this position with $\mathbb{E}$, and search for the input in $Q$ with a transition $Q \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \mathit{in} P'$, where $\mathbb{G}$ is the context surrounding $Q$ up to the parallel composition (initially ●), and $\mathfrak{F}$ records if the continuation $K$ is to the left (then $\mathfrak{F} = K \|$) or to the right (then $\mathfrak{F} = \|K$) of $Q$ (rules $\mathit{parlnL}$ and $\mathit{parlnR}$).

The in mode is then going through the receiving process, pushing the constructs on the context $\mathbb{G}$ (rules in$\mathit{ParL}$, in$\mathit{ParR}$, $\mathit{parLoc}$, and in$\mathit{Nu}$). Once the input $a(X).R$ has been found, all the pieces have been collected for the communication to happen, resulting in $\mathbb{E}[\nu \vec{b} . \mathfrak{F}[\mathbb{G}[R\{M/X\}]]]$. For instance, if we start from a process $\mathbb{E}[\mathbb{F}[\bar{a}\langle M\rangle K] \| \mathbb{G}[a(X).R]]$, then $\mathfrak{F} = \mathbb{F}'[K] \|$ where $\mathbb{F}'$ is what is left from $\mathbb{F}$ after removing the restricted names $\vec{b}$.

## 2.4 Properties of the Leaf-First Semantics

*Correspondence results.* We state how the leaf-first zipper semantics relates to the lazy semantics of $\text{HO}_\pi\text{P}$; the proofs can be found in Appendix A.

**Theorem 1.** If $R \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \mathit{in} P'$, then $R \xrightarrow{a(M)} R'$ for some $R'$ and $P' = \mathbb{E}[\nu \vec{b} . \mathfrak{F}[\mathbb{G}[R']]]$. If $\mathbb{E} \xrightarrow{K, \vec{b}, a, M} \mathit{par} P'$, then for all $S \xrightarrow{\nu \vec{b} . \bar{a}\langle M\rangle} K$, we have $\mathbb{E}[S] \xrightarrow{\tau} P'$. If $P \xrightarrow{\mathbb{E}} \mathit{out} P'$, then $\mathbb{E}[P] \xrightarrow{\tau} P'$.

From the last item, we deduce that $P \xrightarrow{\tau} \mathit{zs} P'$ implies $P \xrightarrow{\tau} P'$. For the reverse implication, given $P \xrightarrow{\tau} P'$, we make explicit the contexts in $P$ and $P'$, writing them as $P = \mathbb{E}[\mathbb{H}[\bar{a}\langle M\rangle K] \| R]$ and $P' = \mathbb{E}[\nu \vec{b} . \mathbb{G}[K] \| R']$, with $R \xrightarrow{a(M)} R'$, and $\mathbb{H}$ built from $\vec{b}$ and $\mathbb{G}$. From there, we can reconstruct the zipper derivation; the proof is in the appendix.

**Theorem 2.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\mathit{zs}} P'$.
$\mathbb{E} \xrightarrow{K, \vec{b}, a, M} \mathit{par} P'$ goes through $\mathbb{E}$ looking for the parallel composition, constructing $K$ (the continuation of the output) and $\vec{b}$ (the extruded names) while doing so, and remembering that $M$ is sent on $a$. The rules `outOut` and `outPassiv` initialize the `par` mode with the proper continuation and with an empty sequence of extruded names. If the context is of the form $\nu c::\mathbb{E}$, the name restriction $\nu c$ surrounds the message output, so we should check that it does not prevent the communication on $a$, hence the premise $c \neq a$ in rules `parNu` and `parExtr`. If $c$ occurs free in the message $M$, it must be extruded, and it is added to the sequence $\vec{b}$ in the rule `parExtr`. Otherwise, it is added to $K$ in the rule `parNu`.

A locality is moved from the context to the continuation (rule `parLoc`). If the context is of the shape $\|Q::\mathbb{E}$ or $Q::\mathbb{E}$, we consider a process of the form $\mathbb{E}[K \| Q]$ or $\mathbb{E}[Q \| K]$ and we have two possibilities. If $Q$ is not the process receiving the message, then $Q$ has to be added to the continuation, and we continue searching for the receiver in $\mathbb{E}$ (rules `parL` and `parR`). Otherwise, we have found the parallel composition where the communication takes place, which is where the extruded names $\vec{b}$ should be restricted. We remember this position with $\mathbb{E}$, and search for the input in $Q$ with a transition $Q \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \mathit{in} P'$, where $\mathbb{G}$ is the context surrounding $Q$ up to the parallel composition (initially $\bullet$), and $\mathfrak{F}$ records if the continuation $K$ is to the left (then $\mathfrak{F} = K \|$) or to the right (then $\mathfrak{F} = \|K$) of $Q$ (rules `parInL` and `parInR`).

The `in` mode is then going through the receiving process, pushing the constructs on the context $\mathbb{G}$ (rules `inParL`, `inParR`, `parLoc`, and `inNu`). Once the input $a(X).R$ has been found, all the pieces have been collected for the communication to happen, resulting in $\mathbb{E}[\nu \vec{b} . \mathfrak{F}[\mathbb{G}[R\{M/X\}]]]$. For instance, if we start from a process $\mathbb{E}[\mathbb{F}[\bar{a}\langle M \rangle K] \| \mathbb{G}[a(X).R]]$, then $\mathfrak{F} = \mathbb{F}'[K] \|$ where $\mathbb{F}'$ is what is left from $\mathbb{F}$ after removing the restricted names $\vec{b}$.

## 2.4 Properties of the Leaf-First Semantics

*Correspondence results.* We state how the leaf-first zipper semantics relates to the lazy semantics of $HO\pi P$; the proofs can be found in Appendix A.

**Theorem 1.** If $R \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \mathit{in} P'$, then $R \xrightarrow{a(M)} R'$ for some $R'$ and $P' = \mathbb{E}[\nu \vec{b} . \mathfrak{F}[\mathbb{G}[R']]]$. If $\mathbb{E} \xrightarrow{K, \vec{b}, a, M} \mathit{par} P'$, then for all $S \xrightarrow{\nu \vec{b} . \bar{a}\langle M \rangle} K$, we have $\mathbb{E}[S] \xrightarrow{\tau} P'$. If $P \xrightarrow{\mathbb{E}} \mathit{out} P'$, then $\mathbb{E}[P] \xrightarrow{\tau} P'$.

From the last item, we deduce that $P \xrightarrow{\tau} \mathit{zs} P'$ implies $P \xrightarrow{\tau} P'$. For the reverse implication, given $P \xrightarrow{\tau} P'$, we make explicit the contexts in $P$ and $P'$, writing them as $P = \mathbb{E}[\mathbb{H}[\bar{a}\langle M \rangle K] \| R]$ and $P' = \mathbb{E}[\nu \vec{b} . \mathbb{G}[K] \| R']$, with $R \xrightarrow{a(M)} R'$, and $\mathbb{H}$ built from $\vec{b}$ and $\mathbb{G}$. From there, we can reconstruct the zipper derivation; the proof is in the appendix.

**Theorem 2.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\mathit{zs}} P'$.
*Derivation into a NDAM.* The semantics of Figure 2 fits the zipper semantics generic format [3]: each traversing rule (distinct from *init* and *inCom*) has exactly one premise, and is decomposing its source term one operator at a time.

A zipper semantics can be derived into an NDAM if it satisfies some properties, like being *machine constructive*: in each rule, it should be possible to construct the terms in the premise from those of the conclusion. This property holds if the meta-variables (of processes, contexts, names, etc) of the premise are included in those of the conclusion, as one can check in Figure 2. The semantics should also be *reversible*: conversely, we can recreate the terms in the conclusion from the premise, to allow for backtracking. It is the case because for each rule, the meta-variables of the conclusion are included in those of the premise.

Finally, the zipper semantics must be *terminating*, ensuring that the search for a redex in the NDAM does not infinitely loop. To prove it, it is enough to exhibit a strictly decreasing size on transitions such that the size of the premise is smaller than its conclusion. For each rule, the source term of the premise is a subterm of the source term of the conclusion, except when changing mode. We therefore consider a lexicographic ordering on modes first, so that out > par > in, and then on the size of the source term of the transition.

## 3 HOπ with Join Patterns

We consider HOπJ, an extension of HOπ with join patterns [11], where an input may receive an arbitrary number of messages simultaneously.

### 3.1 Syntax and Lazy Semantics

*Syntax and informal semantics.* We let $\xi$ range over *message patterns*, which can be seen as multisets of elementary inputs $a_1(X_1) | \dots | a_n(X_n)$ where the $X_i$ are pairwise distinct. We change the input process with $\xi \triangleright R$.

$$ \xi ::= a(X) \mid \xi \mid \xi \quad P, Q, \dots ::= X \mid \mathbf{0} \mid P \parallel Q \mid \xi \triangleright R \mid \bar{a}\langle M \rangle K \mid \nu a.P $$

A communication happens when enough message outputs are in parallel to fulfil the message pattern of an input. Like in HOπ or HOπP, name restriction delimits the scope of names, and lazy scope extrusion may be necessary during communication. However, to keep it as lazy as possible, restricted names should not be extruded further than the parallel composition enclosing the sender and receiver. Consider the following example, where $\xi = a_1(X_1) | a_2(X_2) | a_3(X_3) | a_4(X_4)$ and we abbreviate $\bar{b}\langle \mathbf{0} \rangle \mathbf{0}$ as $\bar{b}$ for any $b$. We number the parallel compositions in the redex, which has the same parallel structure as in Figure 4.

$$ P \parallel ((\nu b.\bar{a}_1\langle \bar{b} \rangle K_1) \parallel^2 (\nu c.\nu d.\bar{a}_2\langle \mathbf{0} \rangle K_2) \parallel^3 \bar{a}_3\langle \bar{d} \rangle K_3) \parallel^1 ((\nu e.\bar{a}_4\langle \bar{e} \rangle K_4) \parallel^4 \xi \triangleright R) \\ \xrightarrow{\tau} P \parallel \nu b.\nu d.((K_1) \parallel^2 (\nu c. K_2) \parallel^3 K_3) \parallel^1 \nu e. (K_4) \parallel^4 R') $$

The scope of *c* is unchanged, while *b* and *d* have been extruded to include $\parallel^1$, and *e* to include $\parallel^4$.
*Derivation into a NDAM.* The semantics of Figure 2 fits the zipper semantics generic format [3]: each traversing rule (distinct from *init* and *inCom*) has exactly one premise, and is decomposing its source term one operator at a time.

A zipper semantics can be derived into an NDAM if it satisfies some properties, like being *machine constructive*: in each rule, it should be possible to construct the terms in the premise from those of the conclusion. This property holds if the meta-variables (of processes, contexts, names, etc) of the premise are included in those of the conclusion, as one can check in Figure 2. The semantics should also be *reversible*: conversely, we can recreate the terms in the conclusion from the premise, to allow for backtracking. It is the case because for each rule, the meta-variables of the conclusion are included in those of the premise.

Finally, the zipper semantics must be *terminating*, ensuring that the search for a redex in the NDAM does not infinitely loop. To prove it, it is enough to exhibit a strictly decreasing size on transitions such that the size of the premise is smaller than its conclusion. For each rule, the source term of the premise is a subterm of the source term of the conclusion, except when changing mode. We therefore consider a lexicographic ordering on modes first, so that out > par > in, and then on the size of the source term of the transition.

## 3 HOπ with Join Patterns

We consider HOπJ, an extension of HOπ with join patterns [11], where an input may receive an arbitrary number of messages simultaneously.

### 3.1 Syntax and Lazy Semantics

*Syntax and informal semantics.* We let $\xi$ range over *message patterns*, which can be seen as multisets of elementary inputs $a_1(X_1) | \dots | a_n(X_n)$ where the $X_i$ are pairwise distinct. We change the input process with $\xi \triangleright R$.

$$ \xi ::= a(X) \mid \xi \mid \xi \quad P, Q, \dots ::= X \mid \mathbf{0} \mid P \parallel Q \mid \xi \triangleright R \mid \bar{a}\langle M \rangle K \mid \nu a.P $$

A communication happens when enough message outputs are in parallel to fulfil the message pattern of an input. Like in HOπ or HOπP, name restriction delimits the scope of names, and lazy scope extrusion may be necessary during communication. However, to keep it as lazy as possible, restricted names should not be extruded further than the parallel composition enclosing the sender and receiver. Consider the following example, where $\xi = a_1(X_1) | a_2(X_2) | a_3(X_3) | a_4(X_4)$ and we abbreviate $\bar{b}\langle \mathbf{0} \rangle \mathbf{0}$ as $\bar{b}$ for any $b$. We number the parallel compositions in the redex, which has the same parallel structure as in Figure 4.

$$ P \parallel ((\nu b.\bar{a}_1\langle \bar{b} \rangle K_1) \parallel^2 (\nu c.\nu d.\bar{a}_2\langle \mathbf{0} \rangle K_2) \parallel^3 (\bar{a}_3\langle \bar{d} \rangle K_3)) \parallel^1 ((\nu e.\bar{a}_4\langle \bar{e} \rangle K_4) \parallel^4 \xi \triangleright R) \\ \xrightarrow{\tau} P \parallel \nu b.\nu d.((K_1) \parallel^2 (\nu c. K_2) \parallel^3 K_3)) \parallel^1 (\nu e. (K_4) \parallel^4 R') $$

The scope of *c* is unchanged, while *b* and *d* have been extruded to include $\parallel^1$, and *e* to include $\parallel^4$.
*Lazy semantics.* We let $p$ range over pairs $(a, M)$ of a message and its output channel. Given a sequence $\vec{p}$, we define the sequence of communication names inductively so that $cn(()) \stackrel{\Delta}{=} ()$ and $cn((a, M) \cdot \vec{p}) \stackrel{\Delta}{=} a \cdot cn(\vec{p})$, and the set of message names as $mn(()) \stackrel{\Delta}{=} \emptyset$ and $mn((a, M) \cdot \vec{p}) \stackrel{\Delta}{=} fn(M) \cup mn(\vec{p})$.

We assume an operator $\xi \bullet \vec{p}$ which checks that there are as many messages in $\vec{p}$ as names in the pattern $\xi$ and computes the possible matchings as substitutions. For example, $a(X) | a(Y) \bullet (a, P)$, $(a, Q)$ generates $X \mapsto P, Y \mapsto Q$ and $X \mapsto Q, Y \mapsto P$. We let $\theta$ range over these substitutions, and write $\theta \in \xi \bullet \vec{p}$ when $\theta$ is a possible matching between $\xi$ and $\vec{p}$, the latter considered as a multiset. Formally, we write $\cup$ for the multiset union, and we define $a(X) \bullet (a, M) \stackrel{\Delta}{=} \{x \mapsto M\}$ and $(\xi_1 | \xi_2) \bullet \vec{p} \stackrel{\Delta}{=} \{\theta_1 \cup \theta_2 \mid \theta_1 \in \xi_1 \bullet \vec{p}_1, \theta_2 \in \xi_2 \bullet \vec{p}_2, \vec{p} = \vec{p}_1 \cup \vec{p}_2\}$.<fnref n="4" />

We define a labeled semantics for HO$\pi$J in Figure 3. Pure input transitions $P \xrightarrow{\vec{p}}_i R$ describe a process $P$ inputting the messages $\vec{p}$ to yield $R$. Pure output transitions $S \xrightarrow{\nu \vec{b} \cdot \vec{p}}_o K$ describe a process $S$ emitting the messages $\vec{p}$ with extruded names $\vec{b}$ to yield $K$. Mixed input/output transitions $P \xrightarrow{\vec{p}}_{io} P'$ describe a process $P$ that emits some messages which, combined with messages $\vec{p}$, trigger an input and result in $P'$. Finally, silent transitions $P \xrightarrow{\tau} P'$ describe a process that does an internal communication: we define them as a notation, standing for $P \xrightarrow[\to io]{0} P'$, an input/output transition with no message received.

A derivation tree of a transition is best described following a path from the root of the source process to the receiver. Upon encountering a name restriction in input/output mode (rule IONU), we check that it does not prevent communication. For a parallel composition, there are two cases: either one of the process is not involved in the communication (rule IOPAR), or it is. In that case, one process must only contain outputs, while the other either contains both an input and outputs (rule IOBOTHIO), or only an input (rule IOBOTHIN). In both cases, the messages and extruded names are collected in the output-only premise, and these messages $\vec{p}$ are added to the ones $\vec{q}$ received up to this point in the other premise. The name restrictions are restored at this point, as it is the parallel composition closest to both the newly collected messages and the input.

On the output-only side, messages are collected by rule OUTOUT; name restrictions are either added to the label for extrusion with rule OUTEXTR, or left in place in rule OUTNU; parallel composition either explores both processes, merging their results (rule OUTBOTH), or only one of them (rule OUTPAR). Note that output rules always collect at least one message.

On the input-only side, name restrictions are left in place (rule INNU), parallel processes only result in the exploration of one of them as there is a single input (rule INPAR), and the actual communication occurs in rule COM, where the collected messages are matched against the input pattern. Input/output rules and input-only rules are very similar and could be merged. We keep them separate as it simplifies the proof that the zipper and lazy semantics coincide.

<footnote n="4">⁴ As bound variables in a join pattern are distinct, $\theta_1$ and $\theta_2$ have disjoint domains.</footnote>
*Lazy semantics.* We let $p$ range over pairs $(a, M)$ of a message and its output channel. Given a sequence $\overrightarrow{p}$, we define the sequence of communication names inductively so that $cn(()) \stackrel{\Delta}{=} ()$ and $cn((a, M) \cdot \overrightarrow{p}) \stackrel{\Delta}{=} a \cdot cn(\overrightarrow{p})$, and the set of message names as $mn(()) \stackrel{\Delta}{=} \emptyset$ and $mn((a, M) \cdot \overrightarrow{p}) \stackrel{\Delta}{=} fn(M) \cup mn(\overrightarrow{p})$.

We assume an operator $\xi \bullet \overrightarrow{p}$ which checks that there are as many messages in $\overrightarrow{p}$ as names in the pattern $\xi$ and computes the possible matchings as substitutions. For example, $a(X) | a(Y) \bullet (a, P)$, $(a, Q)$ generates $X \mapsto P, Y \mapsto Q$ and $X \mapsto Q, Y \mapsto P$. We let $\theta$ range over these substitutions, and write $\theta \in \xi \bullet \overrightarrow{p}$ when $\theta$ is a possible matching between $\xi$ and $\overrightarrow{p}$, the latter considered as a multiset. Formally, we write $\cup$ for the multiset union, and we define $a(X) \bullet (a, M) \stackrel{\Delta}{=} \{x \mapsto M\}$ and $(\xi_1 | \xi_2) \bullet \overrightarrow{p} \stackrel{\Delta}{=} \{\theta_1 \cup \theta_2 \mid \theta_1 \in \xi_1 \bullet \overrightarrow{p}_1, \theta_2 \in \xi_2 \bullet \overrightarrow{p}_2, \overrightarrow{p} = \overrightarrow{p}_1 \cup \overrightarrow{p}_2\}$.<fnref n="4" />

We define a labeled semantics for HO$\pi$J in Figure 3. Pure input transitions $P \xrightarrow{\overrightarrow{p}}_i R$ describe a process $P$ inputting the messages $\overrightarrow{p}$ to yield $R$. Pure output transitions $S \xrightarrow{\nu \overrightarrow{b} \cdot \overrightarrow{p}}_o K$ describe a process $S$ emitting the messages $\overrightarrow{p}$ with extruded names $\overrightarrow{b}$ to yield $K$. Mixed input/output transitions $P \xrightarrow{\overrightarrow{p}}_{io} P'$ describe a process $P$ that emits some messages which, combined with messages $\overrightarrow{p}$, trigger an input and result in $P'$. Finally, silent transitions $P \xrightarrow{\tau} P'$ describe a process that does an internal communication: we define them as a notation, standing for $P \xrightarrow[\to io]{0} P'$, an input/output transition with no message received.

A derivation tree of a transition is best described following a path from the root of the source process to the receiver. Upon encountering a name restriction in input/output mode (rule IONU), we check that it does not prevent communication. For a parallel composition, there are two cases: either one of the process is not involved in the communication (rule IOPAR), or it is. In that case, one process must only contain outputs, while the other either contains both an input and outputs (rule IOBOTHIO), or only an input (rule IOBOTHIN). In both cases, the messages and extruded names are collected in the output-only premise, and these messages $\overrightarrow{p}$ are added to the ones $\overrightarrow{q}$ received up to this point in the other premise. The name restrictions are restored at this point, as it is the parallel composition closest to both the newly collected messages and the input.

On the output-only side, messages are collected by rule OUTOUT; name restrictions are either added to the label for extrusion with rule OUTEXTR, or left in place in rule OUTNU; parallel composition either explores both processes, merging their results (rule OUTBOTH), or only one of them (rule OUTPAR). Note that output rules always collect at least one message.

On the input-only side, name restrictions are left in place (rule INNU), parallel processes only result in the exploration of one of them as there is a single input (rule INPAR), and the actual communication occurs in rule COM, where the collected messages are matched against the input pattern. Input/output rules and input-only rules are very similar and could be merged. We keep them separate as it simplifies the proof that the zipper and lazy semantics coincide.

<footnote n="4">⁴ As bound variables in a join pattern are distinct, $\theta_1$ and $\theta_2$ have disjoint domains.</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 3. Lazy Semantics for HOπJ</figcaption></figure>

## 3.2 Leaf-First Zipper semantics

Informal description. The HOπJ zipper semantics collects all the messages by alternating between the out and par modes, before looking for the input. During the search, we record the positions where the extruded names should be restricted using contexts stored in a global stack. We also use a local stack to record checkpoints when collecting several messages in a row. We illustrate how the search proceeds using the process in Figure 4, where we represent only the communicating outputs and input, and number the parallel compositions between them. The dotted lines show the exploration of the term within the out mode in red and the par mode in blue.

We start by looking for an output, say $M_1$ (step 1), and then switch to the par mode to look for $\|^2$, computing $K_1$ and extruded names $\vec{b}_1$ while doing so (step 2). We create a checkpoint $(\vec{b}_1, M_1, E_2, K_1)$ on the local stack, where $E_2$ represents the position of $\|^2$, and then look for the next message $M_2$. After finding it (step 3), we go back to $\|^3$ (step 4), computing $K_2$ and $\vec{b}_2$. We create a checkpoint $(\vec{b}_2, M_2, E_{32}, K_2)$ on the local stack, where $E_{32}$ represents the position of $\|^3$ relative to $\|^2$, before searching for $M_3$ (step 5). We then go back to $\|^3$, computing $K_3$ and $\vec{b}_3$ (step 6).
<figure><img src="image_5.png" /><figcaption>Fig. 3. Lazy Semantics for HOπJ</figcaption></figure>

## 3.2 Leaf-First Zipper semantics

*Informal description.* The HOπJ zipper semantics collects all the messages by alternating between the out and par modes, before looking for the input. During the search, we record the positions where the extruded names should be restricted using contexts stored in a global stack. We also use a local stack to record checkpoints when collecting several messages in a row. We illustrate how the search proceeds using the process in Figure 4, where we represent only the communicating outputs and input, and number the parallel compositions between them. The dotted lines show the exploration of the term within the out mode in red and the par mode in blue.

We start by looking for an output, say $M_1$ (step 1), and then switch to the par mode to look for $\|^2$, computing $K_1$ and extruded names $\vec{b}_1$ while doing so (step 2). We create a checkpoint $(\vec{b}_1, M_1, E_2, K_1)$ on the local stack, where $E_2$ represents the position of $\|^2$, and then look for the next message $M_2$. After finding it (step 3), we go back to $\|^3$ (step 4), computing $K_2$ and $\vec{b}_2$. We create a checkpoint $(\vec{b}_2, M_2, E_{32}, K_2)$ on the local stack, where $E_{32}$ represents the position of $\|^3$ relative to $\|^2$, before searching for $M_3$ (step 5). We then go back to $\|^3$, computing $K_3$ and $\vec{b}_3$ (step 6).
<figure><img src="image_4.png" /><figcaption>Fig. 4. Example of Process Exploration</figcaption></figure>

To continue exploring, we pop the local stack to get back $\mathbb{E}_{32}$. We also combine the continuations $K_{23} = K_2 \| K_3$ and the names $\overrightarrow{b_{23}} = \overrightarrow{b_2} \cdot \overrightarrow{b_3}$. We go through $\mathbb{E}_{32}$ (step 7) to get back to $\|^2$. We pop the local stack again to get $\mathbb{E}_2$ and create $K_{123} = K_1 \| K_{23}$ and $\overrightarrow{b_{123}} = \overrightarrow{b_1} \cdot \overrightarrow{b_{23}}$. The search goes through $\mathbb{E}_2$ to find $\|^1$ (step 8). Because $\|^1$ separates $M_1, M_2$, and $M_3$ from the input, it is where $\overrightarrow{b_{123}}$ should be restricted: we create a checkpoint $(\overrightarrow{b_{123}}, (M_1, M_2, M_3), \mathbb{E}_1, K_{123})$ on the global stack, where $\mathbb{E}_1$ records the position of $\|^1$.

We search for $M_4$ (step 9), then go back to $\|^4$, building $K_4$ and $\overrightarrow{b_4}$ (step 10). Because $\|^4$ is where we restrict $\overrightarrow{b_4}$, we add a checkpoint $(\overrightarrow{b_4}, M_4, \mathbb{E}_{41}, K_4)$ on the global stack, where $\mathbb{E}_{41}$ records the position of $\|^4$ relative to $\|^1$. We then look for the input $R$ and compute the result $\mathbb{E}_1[[\nu\overrightarrow{b_{123}}.K_{123}] \|^1 \mathbb{E}_{41}[[\nu\overrightarrow{b_4}.K_4] \|^4 R']]]$ for some $R'$ by repeatedly popping the global stack (step 11).

This derivation collects the messages in the order $M_1, M_2, M_3, M_4$. It is possible to collect them in the order $M_1, M_3, M_2, M_4$, or $M_2, M_3, M_1, M_4$, or $M_3, M_2, M_1, M_4$. However, the design of the zipper rules forbids the remaining orders. Roughly, when considering the topmost parallel composition (here $\|^1$), the search starts on the other side of the input, so starting with $M_4$ is not possible. Besides, we go from one message to the nearest one, so starting from $M_2$, it is not possible to go to $M_1$ and then back to $M_3$.

*Formal definitions.* The zipper semantics of HO$\pi$J is defined in Figure 5. To make it reversible, we need more complex data structures than just sequences to collect extruded names and messages; we explain why in Section 3.3. We define a structure of names $\hat{a}$ and of pairs $\tilde{p}$ as follows:

$$ \hat{a}, \hat{b} ::= () \mid a \cdot \hat{b} \mid \hat{a} \| \hat{b} \quad \tilde{p}, \tilde{q} ::= (a, P) \mid \tilde{p} \| \tilde{q} $$

We abbreviate a structure $a_1 \dots a_n \cdot ()$ as $(a_1, \dots, a_n)$ or $\overrightarrow{a}$. These structures reflect the process from which they are generated. For example, the structures cor-
<figure><img src="image_6.png" /><figcaption>Fig. 4. Example of Process Exploration</figcaption></figure>

To continue exploring, we pop the local stack to get back $\mathbb{E}_{32}$. We also combine the continuations $K_{23} = K_2 \| K_3$ and the names $\overrightarrow{b_{23}} = \overrightarrow{b_2} \cdot \overrightarrow{b_3}$. We go through $\mathbb{E}_{32}$ (step 7) to get back to $\|^{2}$. We pop the local stack again to get $\mathbb{E}_{2}$ and create $K_{123} = K_1 \| K_{23}$ and $\overrightarrow{b_{123}} = \overrightarrow{b_1} \cdot \overrightarrow{b_{23}}$. The search goes through $\mathbb{E}_{2}$ to find $\|^{1}$ (step 8). Because $\|^{1}$ separates $M_1, M_2$, and $M_3$ from the input, it is where $\overrightarrow{b_{123}}$ should be restricted: we create a checkpoint $(\overrightarrow{b_{123}}, (M_1, M_2, M_3), \mathbb{E}_1, K_{123})$ on the global stack, where $\mathbb{E}_1$ records the position of $\|^{1}$.

We search for $M_4$ (step 9), then go back to $\|^{4}$, building $K_4$ and $\overrightarrow{b_4}$ (step 10). Because $\|^{4}$ is where we restrict $\overrightarrow{b_4}$, we add a checkpoint $(\overrightarrow{b_4}, M_4, \mathbb{E}_{41}, K_4)$ on the global stack, where $\mathbb{E}_{41}$ records the position of $\|^{4}$ relative to $\|^{1}$. We then look for the input $R$ and compute the result $\mathbb{E}_1[[\nu\overrightarrow{b_{123}}.K_{123}] \|^{1} \mathbb{E}_{41}[\nu\overrightarrow{b_4}.K_4] \|^{4} R']]$ for some $R'$ by repeatedly popping the global stack (step 11).

This derivation collects the messages in the order $M_1, M_2, M_3, M_4$. It is possible to collect them in the order $M_1, M_3, M_2, M_4$, or $M_2, M_3, M_1, M_4$, or $M_3, M_2, M_1, M_4$. However, the design of the zipper rules forbids the remaining orders. Roughly, when considering the topmost parallel composition (here $\|^{1}$), the search starts on the other side of the input, so starting with $M_4$ is not possible. Besides, we go from one message to the nearest one, so starting from $M_2$, it is not possible to go to $M_1$ and then back to $M_3$.

*Formal definitions.* The zipper semantics of HO$\pi$J is defined in Figure 5. To make it reversible, we need more complex data structures than just sequences to collect extruded names and messages; we explain why in Section 3.3. We define a structure of names $\hat{a}$ and of pairs $\tilde{p}$ as follows:

$$ \hat{a}, \hat{b} ::= () \mid a \cdot \hat{b} \mid \hat{a} \| \hat{b} \quad \tilde{p}, \tilde{q} ::= (a, P) \mid \tilde{p} \| \tilde{q} $$

We abbreviate a structure $a_1 \dots a_n \cdot ()$ as $(a_1, \dots, a_n)$ or $\overrightarrow{a}$. These structures reflect the process from which they are generated. For example, the structures cor-
<figure><img src="image_5.png" /><figcaption>Fig. 5. Zipper semantics for HOπJ</figcaption></figure>

responding to $\nu a.(\overline{a_1}\langle P_1 \rangle \parallel \nu b.\nu c.\overline{a_2}\langle P_2 \rangle)$ are $a.((\langle b, c \rangle) \text{ and } (a_1, P_1) \parallel (a_2, P_2))$.
We define a flattening $|\cdot|$ from structures back to sequences as follows:

$$ \begin{align*} |()| &\stackrel{\Delta}{=} () & |\hat{a}| \parallel |\hat{b}| &\stackrel{\Delta}{=} |\hat{a}| \cdot |\hat{b}| & |a \cdot \hat{b}| &\stackrel{\Delta}{=} a \cdot |\hat{b}| \\ |(a, P)| &\stackrel{\Delta}{=} (a, P) & |\tilde{a}| \parallel |\tilde{b}| &\stackrel{\Delta}{=} |\tilde{a}| \cdot |\tilde{b}| & & & \end{align*} $$

The syntax of stacks is $\gamma ::= \epsilon$ | $(\hat{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \gamma$ where $\mathfrak{F}$ is either $\parallel K$ or $\parallel K$ for some $K$. We let $\rho$ range over global stacks and $\pi$ over local ones. We extend plugging to global stacks, and define $p(\rho)$ as the pairs occurring in $\rho$.

$$ \begin{align*} \epsilon[\!\!P] &\stackrel{\Delta}{=} P & ((\hat{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \rho)[\!\!P] &\stackrel{\Delta}{=} \rho[\!\!\mathbb{E}[\nu|\hat{a}|.\mathfrak{F}[\!\!P]]] \\ p(\epsilon) &\stackrel{\Delta}{=} () & p((\hat{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \rho) &\stackrel{\Delta}{=} |\tilde{p}| \cdot p(\rho) \end{align*} $$

The rules for the output $P \xrightarrow{\mathbb{E}, \pi, \rho} \text{out} P'$ and input modes $R \xrightarrow{\mathbb{G}, \rho} \text{in} P'$ are roughly the same as in HOπP. The stacks $\pi, \rho$ are passed along without being modified; $\rho$ is used in the axiom inCom to compute the final result. The transition $\mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \pi, \rho} \text{par} P'$ is looking for the nearest parallel composition which separates the last found output to the rest of the redex, building $K$ and $\hat{a}$. The rules, parNu, and parExtr are the same as in HOπP, only adapted to the multiple messages $\tilde{p}$.
<figure><img src="image_7.png" /><figcaption>Fig. 5. Zipper semantics for HOπJ</figcaption></figure>

responding to $\nu a.(\overline{a_1}\langle P_1 \rangle \parallel \nu b.\nu c.\overline{a_2}\langle P_2 \rangle)$ are $a.((\langle b, c \rangle) \text{ and } (a_1, P_1) \parallel (a_2, P_2))$.
We define a flattening $|\cdot|$ from structures back to sequences as follows:

$$ \begin{align*} |()| &\stackrel{\Delta}{=} () & |\hat{a}| \parallel |\hat{b}| &\stackrel{\Delta}{=} |\hat{a}| \cdot |\hat{b}| & |a \cdot \hat{b}| &\stackrel{\Delta}{=} a \cdot |\hat{b}| \\ |(a, P)| &\stackrel{\Delta}{=} (a, P) & |\tilde{a}| \parallel |\tilde{b}| &\stackrel{\Delta}{=} |\tilde{a}| \cdot |\tilde{b}| & & & \end{align*} $$

The syntax of stacks is $\gamma ::= \epsilon$ | $(\hat{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \gamma$ where $\mathfrak{F}$ is either $\parallel K$ or $\parallel K$ for some $K$. We let $\rho$ range over global stacks and $\pi$ over local ones. We extend plugging to global stacks, and define $p(\rho)$ as the pairs occurring in $\rho$.

$$ \begin{align*} \epsilon[\!\!P] &\stackrel{\Delta}{=} P & ((\hat{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \rho)[\!\!P] &\stackrel{\Delta}{=} \rho[\!\!E[\nu|\hat{a}|.\mathfrak{F}[\!\!P]]] \\ p(\epsilon) &\stackrel{\Delta}{=} () & p((\hat{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \rho) &\stackrel{\Delta}{=} |\tilde{p}| \cdot p(\rho) \end{align*} $$

The rules for the output $P \xrightarrow{\mathbb{E},\pi,\rho} \text{out} P'$ and input modes $R \xrightarrow{\mathbb{G},\rho} \text{in} P'$ are roughly the same as in HO$\pi$P. The stacks $\pi, \rho$ are passed along without being modified; $\rho$ is used in the axiom inCom to compute the final result. The transition $\mathbb{E} \xrightarrow{K,\hat{a},\tilde{p},\pi,\rho} \text{par} P'$ is looking for the nearest parallel composition which separates the last found output to the rest of the redex, building $K$ and $\hat{a}$. The rules, parNu, and parExtr are the same as in HO$\pi$P, only adapted to the multiple messages $\tilde{p}$.
When the context is $||P::E$, i.e., the term is $E[[K||P]]$, we have several possibilities. If $P$ is not part of the communication, it is added to the continuation (rule parL). If $P$ contains at least one output but not the input, we apply the rule parOutR to look for the next output in $P$ and create a checkpoint on the local stack. That checkpoint is popped when we apply parHoleL: after finding all the messages in $P$, we restore $E$ to continue the search in that context.

The next possibility is that $P$ contains at least one output and the input: we apply parOutR$\rho$ to look for the next output in $P$ and create a checkpoint on the global stack to remember that $E$ is where the names $\hat{a}$ should be restricted. The rule parOutR$\rho$ applies only when the local stack is empty, meaning that we are done collecting messages on that side of the parallel composition. The final case is when $P$ contains only the input: we switch to the in mode and creates the last checkpoint on the global stack. As in the previous case, the local stack must be empty. We illustrate these rules on the example of Figure 4.

*Back to the example.* We start with empty local and global stacks. After reaching $\overline{a_1}\langle M_1 \rangle$, we go back to $||^2$ to search for the next messages: at that point, the derivation looks like the rule on the left below. The process $P_{23}$ contains $\overline{a_2}\langle M_2 \rangle$ and $\overline{a_3}\langle M_3 \rangle$: we use similar naming convention for processes henceforth. Let $\pi_1 \stackrel{\Delta}{=} (\hat{b}_1, (a_1, M_1), \mathbb{E}_2, K_1 ||^2) :: \epsilon$. We look for $M_2$ and then go back to $||^3$, where we apply parOutR again to search for $M_3$ (right rule).

parOutR

$$ \frac{P_{23} \xrightarrow{\bullet, (\hat{b}_1, (a_1, M_1), \mathbb{E}_2, K_1 ||^2) :: \epsilon, \epsilon} \overline{P}' \quad \overline{\|}^2 P_{23} :: \mathbb{E}_2 \xrightarrow{K_1, \hat{b}_1, (a_1, M_1), \epsilon, \epsilon} \overline{\text{par}} P'} $$

parOutR

$$ \frac{P_3 \xrightarrow{\bullet, (\hat{b}_2, (a_2, M_2), \mathbb{E}_{32}, K_2 ||^3) :: \pi_1, \epsilon} \overline{P}' \quad \overline{\|}^3 P_3 :: \mathbb{E}_{32} \xrightarrow{K_2, \hat{b}_2, (a_2, M_2), \pi_1, \epsilon} \overline{\text{par}} P'} $$

After finding $M_3$, we go back to $||^3$ again and pop the local stack to restore $\mathbb{E}_{32}$ and continue the exploration of the term.

parHoleL

$$ \frac{\mathbb{E}_{32} \xrightarrow{K_2 ||^3 K_3, \hat{b}_2 || \hat{b}_3, (a_2, M_2) || (a_3, M_3), \pi_1, \epsilon} \overline{P}' \quad \overline{\|} K_3, \hat{b}_3, (a_3, M_3), (\hat{b}_2, (a_2, M_2), \mathbb{E}_{32}, K_2 ||^3) :: \pi_1, \epsilon \xrightarrow{\bullet} \overline{\text{par}} P'} $$

We go through $\mathbb{E}_{32}$ to reach $||^2$, and apply parHoleL again to restore $\mathbb{E}_2$.

parHoleL

$$ \frac{\mathbb{E}_2 \xrightarrow{K_1 ||^2 K_{23}, \hat{b}_1 || \hat{b}_{23}, (a_1, M_1) || \widetilde{p}_{23}, \epsilon, \epsilon} \overline{P}' \quad \overline{\|} K_{23}, \hat{b}_{23}, \widetilde{p}_{23}, (\hat{b}_1, (a_1, M_1), \mathbb{E}_2, K_1 ||^2) :: \epsilon, \epsilon \xrightarrow{\bullet} \overline{\text{par}} P'} $$

The next step is when we get to $||^1$, where we create a checkpoint on the global stack (left rule below). Let $\rho_1 \stackrel{\Delta}{=} (\widetilde{b}_{123}, \widetilde{p}_{123}, \mathbb{E}_1, K_{123} ||^1) :: \epsilon$. We then look for $M_4$,
When the context is $||P::E$, i.e., the term is $E[[K||P]]$, we have several possibilities. If $P$ is not part of the communication, it is added to the continuation (rule parL). If $P$ contains at least one output but not the input, we apply the rule parOutR to look for the next output in $P$ and create a checkpoint on the local stack. That checkpoint is popped when we apply parHoleL: after finding all the messages in $P$, we restore $E$ to continue the search in that context.

The next possibility is that $P$ contains at least one output and the input: we apply parOutR$\rho$ to look for the next output in $P$ and create a checkpoint on the global stack to remember that $E$ is where the names $\hat{a}$ should be restricted. The rule parOutR$\rho$ applies only when the local stack is empty, meaning that we are done collecting messages on that side of the parallel composition. The final case is when $P$ contains only the input: we switch to the in mode and creates the last checkpoint on the global stack. As in the previous case, the local stack must be empty. We illustrate these rules on the example of Figure 4.

*Back to the example.* We start with empty local and global stacks. After reaching $\overline{a_1}\langle M_1 \rangle$, we go back to $||^2$ to search for the next messages: at that point, the derivation looks like the rule on the left below. The process $P_{23}$ contains $\overline{a_2}\langle M_2 \rangle$ and $\overline{a_3}\langle M_3 \rangle$: we use similar naming convention for processes henceforth. Let $\pi_1 \stackrel{\Delta}{=} (\hat{b}_1, (a_1, M_1), E_2, K_1 ||^2) :: \epsilon$. We look for $M_2$ and then go back to $||^3$, where we apply parOutR again to search for $M_3$ (right rule).

parOutR

$$ \frac{P_{23} \xrightarrow{\bullet, (\hat{b}_1, (a_1, M_1), E_2, K_1 ||^2) :: \epsilon, \epsilon} \overline{P'} \quad \|^2 P_{23} :: E_2 \xrightarrow{K_1, \hat{b}_1, (a_1, M_1), \epsilon, \epsilon} \overline{P'}_{\text{par}}}{\|^3 P_{23} :: E_2 \xrightarrow{K_1, \hat{b}_1, (a_1, M_1), \epsilon, \epsilon} \overline{P'}_{\text{par}}} $$

parOutR

$$ \frac{P_3 \xrightarrow{\bullet, (\hat{b}_2, (a_2, M_2), E_{32}, K_2 ||^3) :: \pi_1, \epsilon} \overline{P'}_{\text{out}} \quad \|^3 P_3 :: E_{32} \xrightarrow{K_2, \hat{b}_2, (a_2, M_2), \pi_1, \epsilon} \overline{P'}_{\text{par}}}{\|^3 P_3 :: E_{32} \xrightarrow{K_2, \hat{b}_2, (a_2, M_2), \pi_1, \epsilon} \overline{P'}_{\text{par}}} $$

After finding $M_3$, we go back to $||^3$ again and pop the local stack to restore $E_{32}$ and continue the exploration of the term.

parHoleL

$$ \frac{E_{32} \xrightarrow{K_2 ||^3 K_3, \hat{b}_2 || \hat{b}_3, (a_2, M_2) || (a_3, M_3), \pi_1, \epsilon} \overline{P'}_{\text{par}}}{\bullet \xrightarrow{K_3, \hat{b}_3, (a_3, M_3), (\hat{b}_2, (a_2, M_2), E_{32}, K_2 ||^3) :: \pi_1, \epsilon} \overline{P'}_{\text{par}}} $$

We go through $E_{32}$ to reach $||^2$, and apply parHoleL again to restore $E_2$.

parHoleL

$$ \frac{E_2 \xrightarrow{K_1 ||^2 K_{23}, \hat{b}_1 || \hat{b}_{23}, (a_1, M_1) || \widetilde{p}_{23}, \epsilon, \epsilon} \overline{P'}_{\text{par}}}{\bullet \xrightarrow{K_{23}, \hat{b}_{23}, \widetilde{p}_{23}, (\hat{b}_1, (a_1, M_1), E_2, K_1 ||^2) :: \epsilon, \epsilon} \overline{P'}_{\text{par}}} $$

The next step is when we get to $||^1$, where we create a checkpoint on the global stack (left rule below). Let $\rho_1 \stackrel{\Delta}{=} (\widetilde{b}_{123}, \widetilde{p}_{123}, E_1, K_{123} ||^1) :: \epsilon$. We then look for $M_4$,
and go back to $\|^4$, where we create the final checkpoint (right rule).

$$ \begin{array}{c} \text{parOutR}\rho \\ P_{4R} \xrightarrow[\|^1 P_{4R} :: \mathbb{E}_1]{\bullet, \epsilon, (\hat{b}_{123}, \hat{p}_{123}, \mathbb{E}_1, K_{123} \|^1) :: \epsilon} \xrightarrow{\text{out}} P' \\ \xrightarrow[\|^1 P_{4R} :: \mathbb{E}_1]{\bullet, \epsilon, (\hat{b}_{123}, \hat{p}_{123}, \mathbb{E}_1, K_{123} \|^1) :: \epsilon} \xrightarrow{\text{par}} P' \end{array} $$

$$ \begin{array}{c} \text{parInR} \\ P_R \xrightarrow[\|^4 P_R :: \mathbb{E}_{41}]{\bullet, (\hat{b}_4, (a_4, M_4), \mathbb{E}_{41}, K_4 \|^4) :: \rho_1} \xrightarrow{\text{in}} P' \\ \xrightarrow[\|^4 P_R :: \mathbb{E}_{41}]{\bullet, (\hat{b}_4, (a_4, M_4), \epsilon, \rho_1) :: \text{par}} P' \end{array} $$

Let $\rho_2 \stackrel{\Delta}{=} (\hat{b}_4, (a_4, M_4), \mathbb{E}_{41}, K_4 \|^4) :: \rho_1$. Once we find the input, we can compute the final result $P' = \rho_2[\overrightarrow{R'}]$ for some $R'$, and one can check that $\rho_2[\overrightarrow{R'}] = \mathbb{E}_1[\overrightarrow{\nu b_{123}} \cdot K_{123}] \|^1 \mathbb{E}_{41}[\overrightarrow{\nu b_4} \cdot K_4] \|^4 R']$, as wished.

### 3.3 Properties of the Zipper Semantics

*Correspondence results.* The correspondence proofs (in Appendix B) between the zipper and lazy semantics follow the same strategy as in HO$\pi$P: using the information stored in the label, we reconstruct the source and target terms of a zipper transition. For example, for each checkpoint $(\hat{a}, \tilde{p}, \mathbb{E}, K \|)$ :: $\gamma$ of a local or global stack and for any $S \xrightarrow{\nu|\hat{a}|\cdot\tilde{p}}_o K$, we know that the source process at this point is of the form $\mathbb{E}[S \| R]$ and the target process is $\mathbb{E}[\nu|\hat{a}| \cdot K \| R']$, where $R$ and $R'$ are computed recursively from $\gamma$.

**Theorem 3.** If $P \to_{zs} P'$, then $P \xrightarrow{\tau} P'$.

For the reverse implication, for any transition $P \xrightarrow{\tau} P'$, we can decompose $P$ and $P'$ with a global stack $\rho$ and sending processes. We then reconstruct the zipper derivation starting with the input mode, then alternating between the par and out modes for each output, reasoning by induction on the size of $\rho$.

**Theorem 4.** If $P \xrightarrow{\tau} P'$, then $P \to_{zs} P'$.

*Derivation into an NDAM.* The rules of the zipper semantics have been designed to be machine constructive and reversible. In particular, using complex data structures for extruded names and messages ensures that the rules parHoleL and parHoleR are reversible: a structure $\hat{a}_1 \| \hat{a}_2$ uniquely decomposes into $\hat{a}_1$ and $\hat{a}_2$, while a sequence $\overrightarrow{a}$ can be split in two in many ways.

For termination, we consider a lexicographic ordering with three sizes on transitions. The first one is the number of pairs $p$ in the label of the transitions, including the stacks. It is constant on all rules except outOut, where it is strictly increasing between the conclusion and the premise, but bounded by the total number of outputs in the process. The second one is constantly equal to 0 for the out and in modes, and equal to the sum of the sizes of all contexts occurring in the transition (including in stacks) in par mode, where the size of a context is its number of frames plus one. It is designed to be strictly decreasing between the conclusion and the premise on all the rules defining the par mode. In particular for parHoleL and parHoleR, the size of the conclusion is equal to the size of the premise plus one. The last ordering is the subterm ordering for terms at the source of the transition, already used in HO$\pi$P. It is strictly decreasing on the rules of the out and in modes, except outOut which has already been covered. As a result we can derive a sound, complete, and terminating NDAM for HO$\pi$J.
and go back to $\|^4$, where we create the final checkpoint (right rule).

parOutR$\rho$

$$ P_{4R} \xrightarrow{\bullet, \epsilon, (\hat{b}_{123}, \hat{p}_{123}, \mathbb{E}_1, K_{123} \|^{1}) \circled{\circ} \epsilon} \underset{\|^{1} P_{4R} \coloneqq \mathbb{E}_{1} \xrightarrow{K_{123}, \hat{b}_{123}, \hat{p}_{123}, \epsilon, \epsilon} \mathrm{par}}{\rightarrow} P' $$

parInR

$$ P_R \xrightarrow{\bullet, (\hat{b}_4, (a_4, M_4), \mathbb{E}_{41}, K_4 \|^{4}) \circled{\circ} \rho_1} \underset{\|^{4} P_R \coloneqq \mathbb{E}_{41} \xrightarrow{K_4, \hat{b}_4, (a_4, M_4), \epsilon, \rho_1} \mathrm{par}}{\rightarrow} P' $$

Let $\rho_2 \stackrel{\Delta}{\equiv} (\hat{b}_4, (a_4, M_4), \mathbb{E}_{41}, K_4 \|^{4}) \circled{\circ} \rho_1$. Once we find the input, we can compute the final result $P' = \rho_2[\overrightarrow{R'}]$ for some $R'$, and one can check that $\rho_2[\overrightarrow{R'}] = \mathbb{E}_1[\overrightarrow{\nu b_{123}} \cdot K_{123}] \|^{1} \mathbb{E}_{41}[\overrightarrow{\nu b_4} \cdot K_4] \|^{4} R']$, as wished.

### 3.3 Properties of the Zipper Semantics

*Correspondence results.* The correspondence proofs (in Appendix B) between the zipper and lazy semantics follow the same strategy as in HO$\pi$P: using the information stored in the label, we reconstruct the source and target terms of a zipper transition. For example, for each checkpoint $(\hat{a}, \tilde{p}, \mathbb{E}, K \|)$ $\circled{\circ} \gamma$ of a local or global stack and for any $S \xrightarrow{\nu|\hat{a}|\cdot\tilde{p}}_o K$, we know that the source process at this point is of the form $\mathbb{E}[S \| R]$ and the target process is $\mathbb{E}[\nu|\hat{a}| \cdot K \| R']$, where $R$ and $R'$ are computed recursively from $\gamma$.

**Theorem 3.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\tau} P'$.

For the reverse implication, for any transition $P \xrightarrow{\tau} P'$, we can decompose $P$ and $P'$ with a global stack $\rho$ and sending processes. We then reconstruct the zipper derivation starting with the input mode, then alternating between the par and out modes for each output, reasoning by induction on the size of $\rho$.

**Theorem 4.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\tau} \mathbb{E}_s P'$.

*Derivation into an NDAM.* The rules of the zipper semantics have been designed to be machine constructive and reversible. In particular, using complex data structures for extruded names and messages ensures that the rules parHoleL and parHoleR are reversible: a structure $\hat{a}_1 \| \hat{a}_2$ uniquely decomposes into $\hat{a}_1$ and $\hat{a}_2$, while a sequence $\overrightarrow{a}$ can be split in two in many ways.

For termination, we consider a lexicographic ordering with three sizes on transitions. The first one is the number of pairs $p$ in the label of the transitions, including the stacks. It is constant on all rules except outOut, where it is strictly increasing between the conclusion and the premise, but bounded by the total number of outputs in the process. The second one is constantly equal to 0 for the out and in modes, and equal to the sum of the sizes of all contexts occurring in the transition (including in stacks) in par mode, where the size of a context is its number of frames plus one. It is designed to be strictly decreasing between the conclusion and the premise on all the rules defining the par mode. In particular for parHoleL and parHoleR, the size of the conclusion is equal to the size of the premise plus one. The last ordering is the subterm ordering for terms at the source of the transition, already used in HO$\pi$P. It is strictly decreasing on the rules of the out and in modes, except outOut which has already been covered. As a result we can derive a sound, complete, and terminating NDAM for HO$\pi$J.
# 4 Related Work and Conclusion

*Related work.* Section 2.2 discusses the root-first zipper semantics [2] for HOπ with eager scope extrusion. As far as we know, its derived NDAM is the only machine proposed for a variant of HOπ. We discuss next the other machines for higher-order calculi and for calculi with join patterns that we are aware of.

The notion of join patterns comes from the join calculus [11], whose initial semantics takes the form of a *chemical abstract machine*, where messages can be seen as as molecules free to move around in a solution until all the messages required to trigger a join-pattern are present. The machines for the languages with passivation Kell [1] and M [13] (which also features join patterns) also rely on this chemical design, typically implemented as message queues. A major drawback of this approach is that it ignores the syntactic structure of processes, making proofs on such structure quite complex. Our approach, on the other hand, preserves the syntactic structure as much as possible, which allows us to prove an operational correspondence between the lazy and zipper semantics (and therefore the NDAM), and not only an observation-based equivalence [1]. This comes with a cost: as the syntactic structure of the term is preserved, the extruded names may enclose unrelated processes even with lazy scope extrusion. Structural congruence would be able to move these unrelated terms around, at the cost of the operational correspondence proof.

A strength and limitation of the join calculus is that it uses the same construct for restriction, reception, and replication. More precisely, definitions $\xi_1 \triangleright R_1 \wedge \dots \wedge \xi_n \triangleright R_n$ are replicated inputs which restrict the names $\bigcup_i cn(\xi_i)$. As a result, the receivers for a given name are fixed. This reduces the expressive power of the calculus [19], but it allows for efficient implementations as long as join patterns are linear [10]. HOπJ is more permissive, as name restriction and input are separate constructs, and although our approach is not as efficient as the join calculus, our use of zipper semantics lets us derive an abstract machine [3].

*Conclusion.* Zipper semantics decomposes a term into an evaluation context and a redex. Biernacka et al. [2,3] define zipper semantics where the search for the redex starts by the operator at its root; instead, we look for an operator at its leaves. This style is well-suited to express the semantics of calculi with lazy scope extrusion, as knowing the message first lets us limit scope extrusion to the sent names. In particular, we are able to express the semantics of a calculus with join patterns, where the scope of extruded names is not the same for all the messages. As a result, we get for free a sound and complete abstract machine for this language. It shows the expressiveness of leaf-first zipper semantics.

Leaf-first zipper semantics is well-suited when the result of reduction depends on information at the leaves of the redex, like message output w.r.t. scope extrusion. Other examples are distributed calculi which restrict communication through locality boundaries [4–6, 15, 25]. In such cases, we need to know the message contents to determine whether it can be sent outside of a locality, so a leaf-first semantics should be more appropriate.
# 4 Related Work and Conclusion

*Related work.* Section 2.2 discusses the root-first zipper semantics [2] for HOπ with eager scope extrusion. As far as we know, its derived NDAM is the only machine proposed for a variant of HOπ. We discuss next the other machines for higher-order calculi and for calculi with join patterns that we are aware of.

The notion of join patterns comes from the join calculus [11], whose initial semantics takes the form of a *chemical abstract machine*, where messages can be seen as as molecules free to move around in a solution until all the messages required to trigger a join-pattern are present. The machines for the languages with passivation Kell [1] and M [13] (which also features join patterns) also rely on this chemical design, typically implemented as message queues. A major drawback of this approach is that it ignores the syntactic structure of processes, making proofs on such structure quite complex. Our approach, on the other hand, preserves the syntactic structure as much as possible, which allows us to prove an operational correspondence between the lazy and zipper semantics (and therefore the NDAM), and not only an observation-based equivalence [1]. This comes with a cost: as the syntactic structure of the term is preserved, the extruded names may enclose unrelated processes even with lazy scope extrusion. Structural congruence would be able to move these unrelated terms around, at the cost of the operational correspondence proof.

A strength and limitation of the join calculus is that it uses the same construct for restriction, reception, and replication. More precisely, definitions $\xi_1 \triangleright R_1 \wedge \dots \wedge \xi_n \triangleright R_n$ are replicated inputs which restrict the names $\bigcup_i cn(\xi_i)$. As a result, the receivers for a given name are fixed. This reduces the expressive power of the calculus [19], but it allows for efficient implementations as long as join patterns are linear [10]. HOπJ is more permissive, as name restriction and input are separate constructs, and although our approach is not as efficient as the join calculus, our use of zipper semantics lets us derive an abstract machine [3].

*Conclusion.* Zipper semantics decomposes a term into an evaluation context and a redex. Biernacka et al. [2,3] define zipper semantics where the search for the redex starts by the operator at its root; instead, we look for an operator at its leaves. This style is well-suited to express the semantics of calculi with lazy scope extrusion, as knowing the message first lets us limit scope extrusion to the sent names. In particular, we are able to express the semantics of a calculus with join patterns, where the scope of extruded names is not the same for all the messages. As a result, we get for free a sound and complete abstract machine for this language. It shows the expressiveness of leaf-first zipper semantics.

Leaf-first zipper semantics is well-suited when the result of reduction depends on information at the leaves of the redex, like message output w.r.t. scope extrusion. Other examples are distributed calculi which restrict communication through locality boundaries [4–6, 15, 25]. In such cases, we need to know the message contents to determine whether it can be sent outside of a locality, so a leaf-first semantics should be more appropriate.
References

1. Bidinger, P., Schmitt, A., Stefani, J.: An abstract machine for the kell calculus. In: Steffen, M., Zavattaro, G. (eds.) Formal Methods for Open Object-Based Distributed Systems, 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3535, pp. 31–46. Springer (2005)

2. Biernacka, M., Biernacki, D., Lenglet, S., Schmitt, A.: Non-deterministic abstract machines. Tech. Rep. 9475, Inria (2022), available at https://hal.inria.fr/hal-03545768

3. Biernacka, M., Biernacki, D., Lenglet, S., Schmitt, A.: Non-deterministic abstract machines. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. LIPIcs, vol. 243, pp. 7:1–7:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

4. Bugliesi, M., Crafa, S., Merro, M., Sassone, V.: Communication and mobility control in boxed ambients. Inf. Comput. 202(1), 39–86 (2005)

5. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) Foundations of Software Science and Computation Structure, First International Conference, FoSSaCS’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1378, pp. 140–155. Springer (1998)

6. Castagna, G., Vitek, J., Nardelli, F.Z.: The seal calculus. Inf. Comput. 201(1), 1–54 (2005)

7. Danvy, O.: From reduction-based to reduction-free normalization. In: Koopman, P.W.M., Plasmeijer, R., Swierstra, S.D. (eds.) Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures. Lecture Notes in Computer Science, vol. 5832, pp. 66–164. Springer (2008)

8. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992)

9. Fessant, F.L.: JoCaml: conception et implémentation d'un langage à agents mobiles. Ph.D. thesis, École polytechnique (2001)

10. Fessant, F.L., Maranget, L.: Compiling join-patterns. In: Nestmann, U., Pierce, B.C. (eds.) 3rd International Workshop on High-Level Concurrent Languages, HLCL 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 12, 1998. pp. 205–224. No. 16(3) in Electronic Notes in Theoretical Computer Science, Elsevier (1998). https://doi.org/10.1016/S1571-0661(04)00143-4, https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/16/issue/3

11. Fournet, C., Gonthier, G.: The reflexive CHAM and the join-calculus. In: Boehm, H., Jr., G.L.S. (eds.) Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996. pp. 372–385. ACM Press (1996)

12. Gardner, P., Laneve, C., Wischik, L.: The fusion machine. In: Brim, L., Jancar, P., Kretínský, M., Kucera, A. (eds.) CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2421, pp. 418–433. Springer (2002)
References

1. Bidinger, P., Schmitt, A., Stefani, J.: An abstract machine for the kell calculus. In: Steffen, M., Zavattaro, G. (eds.) Formal Methods for Open Object-Based Distributed Systems, 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3535, pp. 31–46. Springer (2005)

2. Biernacka, M., Biernacki, D., Lenglet, S., Schmitt, A.: Non-deterministic abstract machines. Tech. Rep. 9475, Inria (2022), available at https://hal.inria.fr/hal-03545768

3. Biernacka, M., Biernacki, D., Lenglet, S., Schmitt, A.: Non-deterministic abstract machines. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. LIPIcs, vol. 243, pp. 7:1–7:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

4. Bugliesi, M., Crafa, S., Merro, M., Sassone, V.: Communication and mobility control in boxed ambients. Inf. Comput. 202(1), 39–86 (2005)

5. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) Foundations of Software Science and Computation Structure, First International Conference, FoSSaCS’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1378, pp. 140–155. Springer (1998)

6. Castagna, G., Vitek, J., Nardelli, F.Z.: The seal calculus. Inf. Comput. 201(1), 1–54 (2005)

7. Danvy, O.: From reduction-based to reduction-free normalization. In: Koopman, P.W.M., Plasmeijer, R., Swierstra, S.D. (eds.) Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures. Lecture Notes in Computer Science, vol. 5832, pp. 66–164. Springer (2008)

8. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992)

9. Fessant, F.L.: JoCaml: conception et implémentation d'un langage à agents mobiles. Ph.D. thesis, École polytechnique (2001)

10. Fessant, F.L., Maranget, L.: Compiling join-patterns. In: Nestmann, U., Pierce, B.C. (eds.) 3rd International Workshop on High-Level Concurrent Languages, HLCL 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 12, 1998. pp. 205–224. No. 16(3) in Electronic Notes in Theoretical Computer Science, Elsevier (1998). https://doi.org/10.1016/S1571-0661(04)00143-4, https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/16/issue/3

11. Fournet, C., Gonthier, G.: The reflexive CHAM and the join-calculus. In: Boehm, H., Jr., G.L.S. (eds.) Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996. pp. 372–385. ACM Press (1996)

12. Gardner, P., Laneve, C., Wischik, L.: The fusion machine. In: Brim, L., Jancar, P., Kretínský, M., Kucera, A. (eds.) CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2421, pp. 418–433. Springer (2002)
13. Germain, F., Lacoste, M., Stefani, J.: An abstract machine for a higher-order distributed process calculus. Electron. Notes Theor. Comput. Sci. **66**(3), 145–169 (2002)

14. Giannini, P., Sangiorgi, D., Valente, A.: Safe ambients: Abstract machine and distributed implementation. Sci. Comput. Program. **59**(3), 209–249 (2006)

15. Godskesen, J.C., Hildebrandt, T.T., Sassone, V.: A calculus of mobile resources. In: Brim, L., Jancar, P., Kretínský, M., Kucera, A. (eds.) CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2421, pp. 272–287. Springer (2002)

16. Hirschkoff, D., Pous, D., Sangiorgi, D.: An efficient abstract machine for safe ambients. J. Log. Algebraic Methods Program. **71**(2), 114–149 (2007)

17. Lenglet, S., Schmitt, A., Stefani, J.: Characterizing contextual equivalence in calculi with passivation. Inf. Comput. **209**(11), 1390–1433 (2011)

18. Lopes, L.M.B., Silva, F.M.A., Vasconcelos, V.T.: A virtual machine for a process calculus. In: Nadathur, G. (ed.) Principles and Practice of Declarative Programming, International Conference PPDP’99, Paris, France, September 29 - October 1, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1702, pp. 244–260. Springer (1999)

19. Nestmann, U.: On the expressive power of joint input. In: Castellani, I., Palamidessi, C. (eds.) Fifth International Workshop on Expressiveness in Concurrency, EXPRESS 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 7, 1998. pp. 145–152. No. 16(2) in Electronic Notes in Theoretical Computer Science, Elsevier (1998). https://doi.org/10.1016/S1571-0661(04)00123-9, https://doi.org/10.1016/S1571-0661(04)00123-9

20. Phillips, A., Cardelli, L.: A correct abstract machine for the stochastic pi-calculus. In: Concurrent Models in Molecular Biology (2004)

21. Phillips, A., Yoshida, N., Eisenbach, S.: A distributed abstract machine for boxed ambient calculi. In: Schmidt, D.A. (ed.) Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2986, pp. 155–170. Springer (2004)

22. Plotkin, G.D.: A structural approach to operational semantics. Tech. Rep. FN-19, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark (Sep 1981)

23. Sangiorgi, D.: Bisimulation in higher-order process calculi. In: Olderog, E. (ed.) Programming Concepts, Methods and Calculi, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET ’94) San Miniato, Italy, 6-10 June, 1994. IFIP Transactions, vol. A-56, pp. 207–224. North-Holland (1994)

24. Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes. Cambridge University Press (2001)

25. Schmitt, A., Stefani, J.: The kell calculus: A family of higher-order distributed process calculi. In: Priami, C., Quaglia, P. (eds.) Global Computing, IST/FET International Workshop, GC 2004, Rovereto, Italy, March 9-12, 2004, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3267, pp. 146–178. Springer (2004)

26. Turner, D.: The Polymorphic Pi-calculus: Theory and Implementation. Ph.D. thesis, University of Edinburgh (1995)
13. Germain, F., Lacoste, M., Stefani, J.: An abstract machine for a higher-order distributed process calculus. Electron. Notes Theor. Comput. Sci. **66**(3), 145–169 (2002)

14. Giannini, P., Sangiorgi, D., Valente, A.: Safe ambients: Abstract machine and distributed implementation. Sci. Comput. Program. **59**(3), 209–249 (2006)

15. Godskesen, J.C., Hildebrandt, T.T., Sassone, V.: A calculus of mobile resources. In: Brim, L., Jancar, P., Kretínský, M., Kucera, A. (eds.) CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2421, pp. 272–287. Springer (2002)

16. Hirschkoff, D., Pous, D., Sangiorgi, D.: An efficient abstract machine for safe ambients. J. Log. Algebraic Methods Program. **71**(2), 114–149 (2007)

17. Lenglet, S., Schmitt, A., Stefani, J.: Characterizing contextual equivalence in calculi with passivation. Inf. Comput. **209**(11), 1390–1433 (2011)

18. Lopes, L.M.B., Silva, F.M.A., Vasconcelos, V.T.: A virtual machine for a process calculus. In: Nadathur, G. (ed.) Principles and Practice of Declarative Programming, International Conference PPDP’99, Paris, France, September 29 - October 1, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1702, pp. 244–260. Springer (1999)

19. Nestmann, U.: On the expressive power of joint input. In: Castellani, I., Palamidessi, C. (eds.) Fifth International Workshop on Expressiveness in Concurrency, EXPRESS 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 7, 1998. pp. 145–152. No. 16(2) in Electronic Notes in Theoretical Computer Science, Elsevier (1998). https://doi.org/10.1016/S1571-0661(04)00123-9, https://doi.org/10.1016/S1571-0661(04)00123-9

20. Phillips, A., Cardelli, L.: A correct abstract machine for the stochastic pi-calculus. In: Concurrent Models in Molecular Biology (2004)

21. Phillips, A., Yoshida, N., Eisenbach, S.: A distributed abstract machine for boxed ambient calculi. In: Schmidt, D.A. (ed.) Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2986, pp. 155–170. Springer (2004)

22. Plotkin, G.D.: A structural approach to operational semantics. Tech. Rep. FN-19, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark (Sep 1981)

23. Sangiorgi, D.: Bisimulation in higher-order process calculi. In: Olderog, E. (ed.) Programming Concepts, Methods and Calculi, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET ’94) San Miniato, Italy, 6-10 June, 1994. IFIP Transactions, vol. A-56, pp. 207–224. North-Holland (1994)

24. Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes. Cambridge University Press (2001)

25. Schmitt, A., Stefani, J.: The kell calculus: A family of higher-order distributed process calculi. In: Priami, C., Quaglia, P. (eds.) Global Computing, IST/FET International Workshop, GC 2004, Rovereto, Italy, March 9-12, 2004, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3267, pp. 146–178. Springer (2004)

26. Turner, D.: The Polymorphic Pi-calculus: Theory and Implementation. Ph.D. thesis, University of Edinburgh (1995)
# A Proofs for HOπP

**Lemma 1.** For all $P \xrightarrow{\tau} P'$, we have $\mathbb{E}[P] \xrightarrow{\tau} \mathbb{E}[P']$.

*Proof.* By induction on $\mathbb{E}$.

**Theorem 5.** The following holds:

1. if $R \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \text{in } P'$, then there exists $R'$ such that $R \xrightarrow{a(M)} R'$ and $P' = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[\mathbb{G}[R']]]$;

2. if $\mathbb{E} \xrightarrow{K, \vec{b}, a, M} \text{par } P'$, then for all $S$ such that $S \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K$, we have $\mathbb{E}[S] \xrightarrow{\tau} P'$;

3. if $P \xrightarrow{\mathbb{E}} \text{out } P'$, then $\mathbb{E}[P] \xrightarrow{\tau} P'$.

*Proof.* We prove the first item by induction on the derivation of $R \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \text{in } P'$. The result holds directly in the case of rule inCom.

For inParL, we have $R_1 \parallel R_2 \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \text{in } P'$ with $R_1 \parallel R_2 :: \mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \text{in } P'$. By the induction hypothesis, there exists $R'_1$ such that $R_1 \xrightarrow{a(M)} R'_1$ and $P' = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[(\parallel R_2 :: \mathbb{G})[R'_1]]]$. But $\mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[(\parallel R_2 :: \mathbb{G})[R'_1]]] = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[\mathbb{G}[R'_1 \parallel R_2]]]$. Because $R_1 \parallel R_2 \xrightarrow{a(M)} R'_1 \parallel R_2$, the result holds with $R' = R'_1 \parallel R_2$. The proof is similar with the rules inParR, inLoc, and inNu.

We prove the second item by induction on the derivation of $\mathbb{E} \xrightarrow{K, \mathbb{F}, a, M} \text{par } P'$.

For parInL, we have $\parallel R :: \mathbb{E} \xrightarrow{K, \vec{b}, a, M} \text{par } P'$ with $R \xrightarrow{\bullet, \vec{b}, a, M, \mathbb{E}, K} \text{in } P'$. By the first item, there exists $R'$ such that $R \xrightarrow{a(M)} R'$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (K \parallel R')]$. Let $S$ such that $S \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K$. Then $(\parallel R :: \mathbb{E})[S] = \mathbb{E}[S \parallel R]$, and we have $\mathbb{E}[S \parallel R] \xrightarrow{\tau} \mathbb{E}[\nu \vec{b} \cdot (K \parallel R')]$ by the communication rule and Lemma 1. The result holds as wished. The proof is similar in the case of parInR.

For parL, we have $\parallel Q :: \mathbb{E} \xrightarrow{K, \vec{b}, a, M} \text{par } P'$ with $\mathbb{E} \xrightarrow{K \parallel Q, \vec{b}, a, M} \text{par } P'$. Let $S$ such that $S \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K$; then $S \parallel Q \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K \parallel Q$. By induction, we have $\mathbb{E}[S \parallel Q] \xrightarrow{\tau} P'$, i.e., $(\parallel Q :: \mathbb{E})[S] \xrightarrow{\tau} P'$, as wished. The proof is similar for parR, parLoc, parNu, and parExtr.

We prove the third item by induction on the derivation of $P \xrightarrow{\mathbb{E}} \text{out } P'$.

For outOut, we have $\bar{a}(M)K \xrightarrow{\mathbb{E}} \text{out } P'$ with $\mathbb{E} \xrightarrow{K((), a, M)} \text{par } P'$. We have $\bar{a}(M)K \xrightarrow{\nu((), \bar{a}(M))} K$, so by the second item, we have directly $\mathbb{E}[\bar{a}(M)K] \xrightarrow{\tau} P'$.

For outPassiv, we have $a[P] \xrightarrow{\mathbb{E}} \text{out } P'$ with $\mathbb{E} \xrightarrow{\mathbf{0}((), a, P)} \text{par } P'$. Because we have $a[P] \xrightarrow{\nu((), \bar{a}(P))} \mathbf{0}$, by the second item, we have directly $\mathbb{E}[a[P]] \xrightarrow{\tau} P'$.
# A Proofs for HOπP

**Lemma 1.** For all $P \xrightarrow{\tau} P'$, we have $\mathbb{E}[P] \xrightarrow{\tau} \mathbb{E}[P']$.

*Proof.* By induction on $\mathbb{E}$.

**Theorem 5.** The following holds:

1. if $R \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \text{in } P'$, then there exists $R'$ such that $R \xrightarrow{a(M)} R'$ and $P' = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[\mathbb{G}[R']]]$;

2. if $\mathbb{E} \xrightarrow{K, \vec{b}, a, M} \text{par } P'$, then for all $S$ such that $S \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K$, we have $\mathbb{E}[S] \xrightarrow{\tau} P'$;

3. if $P \xrightarrow{\mathbb{E}} \text{out } P'$, then $\mathbb{E}[P] \xrightarrow{\tau} P'$.

*Proof.* We prove the first item by induction on the derivation of $R \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \text{in } P'$. The result holds directly in the case of rule inCom.

For inParL, we have $R_1 \parallel R_2 \xrightarrow{\mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \text{in } P'$ with $R_1 \parallel R_2 :: \mathbb{G}, \vec{b}, a, M, \mathbb{E}, \mathfrak{F}} \xrightarrow{\text{in}} P'$. By the induction hypothesis, there exists $R'_1$ such that $R_1 \xrightarrow{a(M)} R'_1$ and $P' = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[(\parallel R_2 :: \mathbb{G})[R'_1]]]$. But $\mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[(\parallel R_2 :: \mathbb{G})[R'_1]]] = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[\mathbb{G}[R'_1 \parallel R_2]]]$. Because $R_1 \parallel R_2 \xrightarrow{a(M)} R'_1 \parallel R_2$, the result holds with $R' = R'_1 \parallel R_2$. The proof is similar with the rules inParR, inLoc, and inNu.

We prove the second item by induction on the derivation of $\mathbb{E} \xrightarrow{K, \mathbb{F}, a, M} \text{par } P'$.

For parInL, we have $\parallel R :: \mathbb{E} \xrightarrow{K, \vec{b}, a, M} \text{par } P'$ with $R \xrightarrow{\bullet, \vec{b}, a, M, \mathbb{E}, K} \text{in } P'$. By the first item, there exists $R'$ such that $R \xrightarrow{a(M)} R'$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (K \parallel R')]$. Let $S$ such that $S \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K$. Then $(\parallel R :: \mathbb{E})[S] = \mathbb{E}[S \parallel R]$, and we have $\mathbb{E}[S \parallel R] \xrightarrow{\tau} \mathbb{E}[\nu \vec{b} \cdot (K \parallel R')]$ by the communication rule and Lemma 1. The result holds as wished. The proof is similar in the case of parInR.

For parL, we have $\parallel Q :: \mathbb{E} \xrightarrow{K, \vec{b}, a, M} \text{par } P'$ with $\mathbb{E} \xrightarrow{K \parallel Q, \vec{b}, a, M} \text{par } P'$. Let $S$ such that $S \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K$; then $S \parallel Q \xrightarrow{\nu \vec{b} \cdot \bar{a}(M)} K \parallel Q$. By induction, we have $\mathbb{E}[S \parallel Q] \xrightarrow{\tau} P'$, i.e., $(\parallel Q :: \mathbb{E})[S] \xrightarrow{\tau} P'$, as wished. The proof is similar for parR, parLoc, parNu, and parExtr.

We prove the third item by induction on the derivation of $P \xrightarrow{\mathbb{E}} \text{out } P'$.

For outOut, we have $\bar{a}(M)K \xrightarrow{\mathbb{E}} \text{out } P'$ with $\mathbb{E} \xrightarrow{K((), a, M)} \text{par } P'$. We have $\bar{a}(M)K \xrightarrow{\nu((), \bar{a}(M))} K$, so by the second item, we have directly $\mathbb{E}[\bar{a}(M)K] \xrightarrow{\tau} P'$.

For outPassiv, we have $a[P] \xrightarrow{\mathbb{E}} \text{out } P'$ with $\mathbb{E} \xrightarrow{\mathbf{0}((), a, P)} \text{par } P'$. Because we have $a[P] \xrightarrow{\nu((), \bar{a}(P))} \mathbf{0}$, by the second item, we have directly $\mathbb{E}[a[P]] \xrightarrow{\tau} P'$.
For outParL, we have $P_1 \parallel P_2 \xrightarrow{\mathbb{E}}_{\text{out}} P'$ with $P_1 \parallel_{P_2 \cdot \mathbb{E}} \xrightarrow{\text{out}} P'$. By induction, we have $(\parallel P_2 \cdot \mathbb{E})[P_1] \xrightarrow{\tau} P'$, i.e., $\mathbb{E}[P_1 \parallel P_2] \xrightarrow{\tau} P'$, as required. The proof is similar for outParR, outLoc, and outNu.

**Corollary 1.** If $P \to_{zs} P'$, then $P \xrightarrow{\tau} P'$.

*Proof.* The transition $P \to_{zs} P'$ implies $P \xrightarrow{\bullet} \mathbb{E}_{\text{out}} P'$, which implies $P \xrightarrow{\tau} P'$ by the third item of the theorem.

**Lemma 2.** If $R \xrightarrow{a(M)} R'$, then for all $G, E, \vec{b}$, and $\mathfrak{F} \in \{P \parallel, \parallel P\}$, we have
$$R \xrightarrow{G, \vec{b}, a, M, E, \mathfrak{F}}_{\text{in}} \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[G[R']]].$$

*Proof.* We proceed by induction on the derivation of $R \xrightarrow{a(M)} R'$. If $R = a(X) \cdot R'$, then the result holds directly by rule inCom.

Suppose $R = R_1 \parallel R_2$ with $R_1 \xrightarrow{a(M)} R'_1$ and $R' = R'_1 \parallel R_2$. By induction, we have $R_1 \xrightarrow{\parallel R_2 \cdot G, \vec{b}, a, M, E, \mathfrak{F}}_{\text{in}} \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[(\parallel R_2 \cdot G)[R'_1]]] = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[G[R'_1 \parallel R_2]]] = \mathbb{E}[\nu \vec{b} \cdot \mathfrak{F}[G[R']]]$. We conclude with the rule inParL. The proofs for the remaining cases are similar.

Given a sequence $\vec{b}$, we write $\vec{b}^{-1}$ for its reverse. Given a context $E$ and a sequence $\vec{b}$, we define the set $E \& \vec{b}$ of their interleavings as follows.

$$ \overline{\bullet \in \bullet \& ()} \qquad \frac{G \in E \& \vec{b}}{\mathfrak{F} :: G \in (\mathfrak{F} :: E) \& \vec{b}} \qquad \frac{G \in E \& \vec{b}}{\nu a. :: G \in E \& (a \cdot \vec{b})} $$

**Lemma 3.** If $E \xrightarrow{G[K], \vec{b}, a, M} \text{par} P'$ and $H \in G \& \vec{b}^{-1}$, then $H ++ E \xrightarrow{K, (), a, M} \text{par} P'$

*Proof.* We proceed by induction on the size of $G$ plus the size of $\vec{b}$. It they are both empty, then the result holds directly.

Let $H \in G \& \vec{b}^{-1}$ such that $H = H' :: \mathfrak{F}$. Suppose $\mathfrak{F}$ is the last frame of $G$, i.e., $G = G' :: \mathfrak{F}$ for some $G'$, and $H' \in G' \& F^{-1}$. We have $E \xrightarrow{\mathfrak{F}[G'[K]], \vec{b}, a, M} \text{par} P'$, which implies $\mathfrak{F} :: E \xrightarrow{G'[K], \vec{b}, a, M} \text{par} P'$ by applying the rule corresponding to the frame (parL, parR, parLoc, or parNu). Otherwise, $\mathfrak{F}$ is the last name of $\vec{b}^{-1}$, i.e., $\mathfrak{F} = \nu c, \vec{b} = c \cdot \vec{b}'$ for some $\vec{b}'$ and $c$, and $H' \in G \& \vec{b}'^{-1}$. We have $E \xrightarrow{G[K], c \cdot \vec{b}', a, M} \text{par} P'$, which implies $\mathfrak{F} :: E \xrightarrow{G[K], \vec{b}', a, M} \text{par} P'$ by applying the rule parExtr.

In both cases, we have $H' ++ \mathfrak{F} :: E \xrightarrow{K, (), a, M} \text{par} P'$ by the induction hypothesis, but $H' ++ \mathfrak{F} :: E = H' :: \mathfrak{F} ++ E = H ++ E$, hence the result holds.

**Lemma 4.** If $P \xrightarrow{\mathbb{E}}_{\text{out}} P'$, then $\mathbb{E}[P] \xrightarrow{\bullet} \mathbb{E}_{\text{out}} P'$.
For outParL, we have $P_1 \parallel P_2 \xrightarrow{\mathbb{E}}_{\text{out}} P'$ with $P_1 \parallel_{P_2 \cdot \mathbb{E}} \xrightarrow{\cdot}_{\text{out}} P'$. By induction, we have $(\parallel P_2 \cdot \mathbb{E})[P_1] \xrightarrow{\tau} P'$, i.e., $\mathbb{E}[P_1 \parallel P_2] \xrightarrow{\tau} P'$, as required. The proof is similar for outParR, outLoc, and outNu.

**Corollary 1.** If $P \xrightarrow{\cdot} \mathbb{z}_S P'$, then $P \xrightarrow{\cdot} \mathbb{P}'$.

*Proof.* The transition $P \xrightarrow{\cdot} \mathbb{z}_S P'$ implies $P \xrightarrow{\bullet} \mathbb{P}'$, which implies $P \xrightarrow{\cdot} \mathbb{P}'$ by the third item of the theorem.

**Lemma 2.** If $R \xrightarrow{a(M)} R'$, then for all $G, E, \vec{b}$, and $\mathfrak{F} \in \{P \parallel, \parallel P\}$, we have
$$R \xrightarrow{G, \vec{b}, a, M, E, \mathfrak{F}}_{\text{in}} E[\nu \vec{b} \cdot \mathfrak{F}[G[R']]].$$

*Proof.* We proceed by induction on the derivation of $R \xrightarrow{a(M)} R'$. If $R = a(X) \cdot R'$, then the result holds directly by rule inCom.

Suppose $R = R_1 \parallel R_2$ with $R_1 \xrightarrow{a(M)} R'_1$ and $R' = R'_1 \parallel R_2$. By induction, we have $R_1 \xrightarrow{\parallel R_2 \cdot G, \vec{b}, a, M, E, \mathfrak{F}}_{\text{in}} E[\nu \vec{b} \cdot \mathfrak{F}[(\parallel R_2 \cdot G)[R'_1]]] = E[\nu \vec{b} \cdot \mathfrak{F}[G[R'_1 \parallel R_2]]] = E[\nu \vec{b} \cdot \mathfrak{F}[G[R']]]$. We conclude with the rule inParL. The proofs for the remaining cases are similar.

Given a sequence $\vec{b}$, we write $\vec{b}^{-1}$ for its reverse. Given a context $E$ and a sequence $\vec{b}$, we define the set $E \& \vec{b}$ of their interleavings as follows.

$$\overline{\bullet \in \bullet \& ()} \qquad \frac{G \in E \& \vec{b}}{\mathfrak{F} :: G \in (\mathfrak{F} :: E) \& \vec{b}} \qquad \frac{G \in E \& \vec{b}}{\nu a. :: G \in E \& (a \cdot \vec{b})}$$

**Lemma 3.** If $E \xrightarrow{G[K], \vec{b}, a, M} \text{par} P'$ and $H \in G \& \vec{b}^{-1}$, then $H ++ E \xrightarrow{K(), a, M} \text{par} P'$

*Proof.* We proceed by induction on the size of $G$ plus the size of $\vec{b}$. It they are both empty, then the result holds directly.

Let $H \in G \& \vec{b}^{-1}$ such that $H = H' :: \mathfrak{F}$. Suppose $\mathfrak{F}$ is the last frame of $G$, i.e., $G = G' :: \mathfrak{F}$ for some $G'$, and $H' \in G' \& F^{-1}$. We have $E \xrightarrow{\mathfrak{F}[G'[K]], \vec{b}, a, M} \text{par} P'$, which implies $\mathfrak{F} :: E \xrightarrow{G'[K], \vec{b}, a, M} \text{par} P'$ by applying the rule corresponding to the frame (parL, parR, parLoc, or parNu). Otherwise, $\mathfrak{F}$ is the last name of $\vec{b}^{-1}$, i.e., $\mathfrak{F} = \nu c, \vec{b} = c \cdot \vec{b}'$ for some $\vec{b}'$ and $c$, and $H' \in G \& \vec{b}'^{-1}$. We have $E \xrightarrow{G[K], c \cdot \vec{b}', a, M} \text{par} P'$, which implies $\mathfrak{F} :: E \xrightarrow{G[K], \vec{b}', a, M} \text{par} P'$ by applying the rule parExtr.

In both cases, we have $H' ++ \mathfrak{F} :: E \xrightarrow{K(), a, M} \text{par} P'$ by the induction hypothesis, but $H' ++ \mathfrak{F} :: E = H' :: \mathfrak{F} ++ E = H ++ E$, hence the result holds.

**Lemma 4.** If $P \xrightarrow{\mathbb{E}} \mathbb{P}'$, then $E[P] \xrightarrow{\bullet} \mathbb{P}'$.
*Proof.* By induction on $\mathbb{E}$.

**Lemma 5.** Let $P \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$. Either there exist $\mathbb{G}$, $\mathbb{H}$, and $K'$ such that $K = \mathbb{G}[K']$, $P = \mathbb{H}[\bar{a} \langle M \rangle K']$, and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$, or there exist $\mathbb{G}$, $\mathbb{H}$ such that $K = \mathbb{G}[0]$, $P = \mathbb{H}[a[M]]$, and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$.

*Proof.* By induction on the derivation of $P \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$. In the base cases, the result holds with $\mathbb{G} = \mathbb{H} = \bullet$.

Suppose $\nu c.P' \xrightarrow{\nu c \cdot \vec{b}' \cdot \bar{a} \langle M \rangle} K$ with $P' \xrightarrow{\nu \vec{b}' \cdot \bar{a} \langle M \rangle} K$ and $c \in \mathrm{fn}(M)$. By induction, suppose there exist $\mathbb{G}$, $\mathbb{H}'$, and $K'$ such that $K = \mathbb{G}[K']$, $P' = \mathbb{H}'[\bar{a} \langle M \rangle K']$, and $\mathbb{H}' \in \mathbb{G} \& \vec{b}'^{-1}$. Then $\mathbb{G}$ and $\mathbb{H} \stackrel{\Delta}{=} \mathbb{H}' :: \nu c$ satisfy the conditions. The proof is the same in the passivation case.

Suppose $P_1 \| P_2 \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K_1 \| P_2$ with $P_1 \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K_1$. By induction, suppose there exist $\mathbb{G}_1$, $\mathbb{H}_1$, and $K'_1$ such that $K_1 = \mathbb{G}_1[K'_1]$, $P_1 = \mathbb{H}_1[\bar{a} \langle Q \rangle K'_1]$, and $\mathbb{H}_1 \in \mathbb{G}_1 \& \vec{b}^{-1}$. Then $\mathbb{G} \stackrel{\Delta}{=} \mathbb{G}_1 :: \| P_2$ and $\mathbb{H} \stackrel{\Delta}{=} \mathbb{H}_1 :: \| P_2$ satisfy the conditions. The proof is the same in the passivation case, and the remaining cases are similar.

**Lemma 6.** If $P \xrightarrow{\tau} P'$, then there exist $S \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$, $R \xrightarrow{a(M)} R'$, and $\mathbb{E}$ such that $P = \mathbb{E}[S \| R]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (K \| R')]$, or $P = \mathbb{E}[R \| S]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (R' \| K)]$.

*Proof.* By induction on the derivation of $P \xrightarrow{\tau} P'$.

**Theorem 6.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\tau} \mathrm{zs} P'$.

*Proof.* By Lemma 6, there exist $S \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$, $R \xrightarrow{a(M)} R'$, and $\mathbb{E}$ such that $P = \mathbb{E}[S \| R]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (K \| R')]$, or $P = \mathbb{E}[R \| S]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (R' \| K)]$. W.l.o.g., we consider the first case, the other being symmetric. Suppose we are in the first case of Lemma 5: there exist $\mathbb{G}$, $\mathbb{H}$, and $K'$ such that $K = \mathbb{G}[K']$, $P = \mathbb{H}[\bar{a} \langle M \rangle K']$, and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$.

By Lemma 2, we have $R \xrightarrow{\bullet, \vec{b}, a, M, \mathbb{E}, K \|} \mathrm{in} \ \mathbb{E}[\nu \vec{b} \cdot (K \| R')] = P'$, which implies $\| R :: \mathbb{E} \xrightarrow{K, \vec{b}, a, M} \mathrm{par} P'$ by rule *parInL*. Because $K = \mathbb{G}[K']$ and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$, we can apply Lemma 3 to get $\mathbb{H} ++ \| R :: \mathbb{E} \xrightarrow{K', \bullet, a, M} \mathrm{par} P'$. From rule *outOut*, we obtain $\bar{a} \langle M \rangle K' \xrightarrow{\mathbb{H} ++ \| R :: \mathbb{E}} \mathrm{out} P'$, and then $(\mathbb{H} ++ \| R :: \mathbb{E})[\bar{a} \langle M \rangle K'] \xrightarrow{\bullet} \mathrm{out} P'$ with Lemma 4. One can check that $P = (\mathbb{H} ++ \| R :: \mathbb{E})[\bar{a} \langle M \rangle K']$, and therefore we have $P \xrightarrow{\mathrm{zs}} P'$, as wished.

If we are in the passivation case of Lemma 5, the reasoning is the same, except we use the rule *outPassiv* after applying Lemma 3.
*Proof.* By induction on $\mathbb{E}$.

**Lemma 5.** Let $P \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$. Either there exist $\mathbb{G}$, $\mathbb{H}$, and $K'$ such that $K = \mathbb{G}[K']$, $P = \mathbb{H}[\bar{a} \langle M \rangle K']$, and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$, or there exist $\mathbb{G}$, $\mathbb{H}$ such that $K = \mathbb{G}[0]$, $P = \mathbb{H}[a[M]]$, and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$.

*Proof.* By induction on the derivation of $P \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$. In the base cases, the result holds with $\mathbb{G} = \mathbb{H} = \bullet$.

Suppose $\nu c.P' \xrightarrow{\nu c \cdot \vec{b}' \cdot \bar{a} \langle M \rangle} K$ with $P' \xrightarrow{\nu \vec{b}' \cdot \bar{a} \langle M \rangle} K$ and $c \in \mathrm{fn}(M)$. By induction, suppose there exist $\mathbb{G}$, $\mathbb{H}'$, and $K'$ such that $K = \mathbb{G}[K']$, $P' = \mathbb{H}'[\bar{a} \langle M \rangle K']$, and $\mathbb{H}' \in \mathbb{G} \& \vec{b}'^{-1}$. Then $\mathbb{G}$ and $\mathbb{H} \stackrel{\Delta}{=} \mathbb{H}' :: \nu c$ satisfy the conditions. The proof is the same in the passivation case.

Suppose $P_1 \| P_2 \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K_1 \| P_2$ with $P_1 \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K_1$. By induction, suppose there exist $\mathbb{G}_1$, $\mathbb{H}_1$, and $K'_1$ such that $K_1 = \mathbb{G}_1[K'_1]$, $P_1 = \mathbb{H}_1[\bar{a} \langle Q \rangle K'_1]$, and $\mathbb{H}_1 \in \mathbb{G}_1 \& \vec{b}^{-1}$. Then $\mathbb{G} \stackrel{\Delta}{=} \mathbb{G}_1 :: \| P_2$ and $\mathbb{H} \stackrel{\Delta}{=} \mathbb{H}_1 :: \| P_2$ satisfy the conditions. The proof is the same in the passivation case, and the remaining cases are similar.

**Lemma 6.** If $P \xrightarrow{\tau} P'$, then there exist $S \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$, $R \xrightarrow{a(M)} R'$, and $\mathbb{E}$ such that $P = \mathbb{E}[S \| R]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (K \| R')]$, or $P = \mathbb{E}[R \| S]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (R' \| K)]$.

*Proof.* By induction on the derivation of $P \xrightarrow{\tau} P'$.

**Theorem 6.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\tau} \mathrm{zs} P'$.

*Proof.* By Lemma 6, there exist $S \xrightarrow{\nu \vec{b} \cdot \bar{a} \langle M \rangle} K$, $R \xrightarrow{a(M)} R'$, and $\mathbb{E}$ such that $P = \mathbb{E}[S \| R]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (K \| R')]$, or $P = \mathbb{E}[R \| S]$ and $P' = \mathbb{E}[\nu \vec{b} \cdot (R' \| K)]$. W.l.o.g., we consider the first case, the other being symmetric. Suppose we are in the first case of Lemma 5: there exist $\mathbb{G}$, $\mathbb{H}$, and $K'$ such that $K = \mathbb{G}[K']$, $P = \mathbb{H}[\bar{a} \langle M \rangle K']$, and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$.

By Lemma 2, we have $R \xrightarrow{\bullet, \vec{b}, a, M, \mathbb{E}, K \|} \mathrm{in} \ \mathbb{E}[\nu \vec{b} \cdot (K \| R')] = P'$, which implies $\| R :: \mathbb{E} \xrightarrow{K, \vec{b}, a, M} \mathrm{par} P'$ by rule *parInL*. Because $K = \mathbb{G}[K']$ and $\mathbb{H} \in \mathbb{G} \& \vec{b}^{-1}$, we can apply Lemma 3 to get $\mathbb{H} ++ \| R :: \mathbb{E} \xrightarrow{K', \bullet, a, M} \mathrm{par} P'$. From rule *outOut*, we obtain $\bar{a} \langle M \rangle K' \xrightarrow{\mathbb{H} ++ \| R :: \mathbb{E}} \mathrm{out} P'$, and then $(\mathbb{H} ++ \| R :: \mathbb{E})[\bar{a} \langle M \rangle K'] \xrightarrow{\bullet} \mathrm{out} P'$ with Lemma 4. One can check that $P = (\mathbb{H} ++ \| R :: \mathbb{E})[\bar{a} \langle M \rangle K']$, and therefore we have $P \xrightarrow{\mathrm{zs}} P'$, as wished.

If we are in the passivation case of Lemma 5, the reasoning is the same, except we use the rule *outPassiv* after applying Lemma 3.
B Proofs for HOπJ

Given a frame $\mathfrak{F}$ of the form $K \parallel$ or $\parallel K$, we define the swapping of $K$ with $S$,
written $\mathfrak{F}\{K/S\}$, as follows.

$$
(K \parallel)\{K/S\} \stackrel{\Delta}{=} S \parallel \quad (\parallel K)\{K/S\} \stackrel{\Delta}{=} S
$$

We then define a special plugging operation on local and global stacks: given a
(local or global) stack $\gamma$, a sequence $\overrightarrow{S}$ of processes to swap in frames, and a
process $P$, we define $(\gamma @ \overrightarrow{S})[P]$ as follows.

$$
\begin{gather*}
(\epsilon @ \text{()})[P] \stackrel{\Delta}{=} P \\
((\tilde{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \gamma @ S \cdot \overrightarrow{S'})[P] \stackrel{\Delta}{=} (\gamma @ \overrightarrow{S'})[\mathbb{E}[\mathfrak{F}\{K/S\}[P]]] \text{ if } \mathfrak{F} = \|K\text{ or } \mathfrak{F} = K\|
\end{gather*}
$$

We first state how zipper transitions relates to lazy transitions.

**Theorem 7.** *The following holds:*

1. if $R \xrightarrow{\mathbb{E},\rho} \mathfrak{P}'$, then there exists $R'$ such that $R \xrightarrow{|\rho(\rho)|} \mathfrak{R}'$ and $P' = \rho[\mathbb{E}[\mathfrak{R}']]$;

2. if $\mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \pi, \rho} \mathfrak{par} P'$, $\pi = (\hat{a}_1^1, \tilde{p}_1^1, \mathbb{E}_1^1, \mathfrak{F}_1^1) :: \dots :: (\hat{a}_n^1, \tilde{p}_1^n, \mathbb{E}_1^n, \mathfrak{F}_1^n) :: \epsilon$, and $\rho = (\hat{a}_2^1, \tilde{p}_2^1, \mathbb{E}_2^1, \mathfrak{F}_2^1) :: \dots :: (\hat{a}_m^1, \tilde{p}_2^m, \mathbb{E}_2^m, \mathfrak{F}_2^m) :: \epsilon$, then for all $S \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} \mathfrak{o}$ $K$ and $S_j^i \xrightarrow{\nu|\hat{a}_j^i|\cdot|\tilde{p}_j^i|} \mathfrak{o}$ $K_j^i$, we have $(\rho @ \overrightarrow{S}_2)[(\pi @ \overrightarrow{S}_1)[\mathbb{E}[S]]] \xrightarrow{\tau} P'$.

3. if $P \xrightarrow{\mathbb{E},\pi,\rho} \mathfrak{out} P'$, $\pi = (\hat{a}_1^1, \tilde{p}_1^1, \mathbb{E}_1^1, \mathfrak{F}_1^1) :: \dots :: (\hat{a}_n^1, \tilde{p}_1^n, \mathbb{E}_1^n, \mathfrak{F}_1^n) :: \epsilon$, and $\rho = (\hat{a}_2^1, \tilde{p}_2^1, \mathbb{E}_2^1, \mathfrak{F}_2^1) :: \dots :: (\hat{a}_m^1, \tilde{p}_2^m, \mathbb{E}_2^m, \mathfrak{F}_2^m) :: \epsilon$, then for all $S_j^i \xrightarrow{\nu|\hat{a}_j^i|\cdot|\tilde{p}_j^i|} \mathfrak{o}$ $K_j^i$, we have $(\rho @ \overrightarrow{S}_2)[(\pi @ \overrightarrow{S}_1)[\mathbb{E}[P]]] \xrightarrow{\tau} P'$.

Proof. The first item is by induction on the derivation of $R \xrightarrow{\mathbb{E},\rho} \mathfrak{P}'$. In the case of the rule inCom, we have $R = \xi \triangleright R''$, $\theta \in \xi \mathbf{.} |\rho(\rho)|$, and $P' = \rho[\mathbb{R}''\theta[]]$. It is easy to check that $R \xrightarrow{|\rho(\rho)|} \mathfrak{o} R''\theta$, hence the result holds with $R' = R''\theta$. The inductive cases are straightforward.

The second and third items are proved by mutual induction on their deriva-
tion. The base cases are rules parInR and parInL; we handle the first one, the other
being symmetric. We have $\|R\::= \mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \epsilon, \rho} \mathfrak{par} P'$ with $R \xrightarrow{\bullet, (\hat{a}, \tilde{p}, \mathbb{E}, K \parallel) :: \rho} \mathfrak{in} P'$.
Let $\rho' = (\hat{a}, \tilde{p}, \mathbb{E}, K \parallel) :: \rho$. By the first item, there exists $R'$ such that $R \xrightarrow{|\rho(\rho')|} \mathfrak{o} R'$
and $P' = \rho'[\mathbb{R}']$. One can prove by induction on $\rho'$ that $(\rho' @ S \cdot \overrightarrow{S}_2)[R] \xrightarrow{\tau} P'$,
but $(\rho' @ S \cdot \overrightarrow{S}_2)[R] = (\rho @ \overrightarrow{S}_2)[\mathbb{E}[K \parallel R]]$, hence the result holds.

Most of the cases are straightforward by induction: parL, parR, parExtr, parNu,
outParL, outParR, and outNu. For outOut, we have $\bar{a}\langle M \rangle K \xrightarrow{\mathbb{E},\pi,\rho} \mathfrak{out} P'$ with
$\mathbb{E} \xrightarrow{K,(),(a,M),\pi,\rho} \mathfrak{par} P'$. Because $\bar{a}\langle M \rangle K \xrightarrow{\nu(),(a,M)} \mathfrak{o} K$, we have $(\rho @ \overrightarrow{S}_2)[\mathbb{E}[\bar{a}\langle M \rangle K]]] \xrightarrow{\tau} P'$ by the induction hypothesis, which is exactly what we
want.
B Proofs for HOπJ

Given a frame $\mathfrak{F}$ of the form $K \parallel$ or $\parallel K$, we define the swapping of $K$ with $S$,
written $\mathfrak{F}\{K/S\}$, as follows.

$$
(K \parallel)\{K/S\} \stackrel{\Delta}{=} S \parallel \quad (\parallel K)\{K/S\} \stackrel{\Delta}{=} S
$$

We then define a special plugging operation on local and global stacks: given a
(local or global) stack $\gamma$, a sequence $\overrightarrow{S}$ of processes to swap in frames, and a
process $P$, we define $(\gamma @ \overrightarrow{S})[P]$ as follows.

$$
\begin{gather*}
(\epsilon @ \text{()})[P] \stackrel{\Delta}{=} P \\
((\hat{a}, \tilde{p}, \mathbb{E}, \mathfrak{F}) :: \gamma @ S \cdot \overrightarrow{S'})[P] \stackrel{\Delta}{=} (\gamma @ \overrightarrow{S'})[\mathbb{E}[\mathfrak{F}\{K/S\}[P]]] \text{ if } \mathfrak{F} = \|K\text{ or } \mathfrak{F} = K\|
\end{gather*}
$$

We first state how zipper transitions relates to lazy transitions.

**Theorem 7.** *The following holds:*

1. if $R \xrightarrow{\mathbb{E},\rho} \mathfrak{P}'$, then there exists $R'$ such that $R \xrightarrow{|\rho(\rho)|} \mathfrak{R}'$ and $P' = \rho[\mathbb{E}[\mathfrak{R}']]$;

2. if $\mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \pi, \rho} \mathfrak{par} P'$, $\pi = (\hat{a}_1^1, \tilde{p}_1^1, \mathbb{E}_1^1, \mathfrak{F}_1^1) :: \dots :: (\hat{a}_n^1, \tilde{p}_1^n, \mathbb{E}_1^n, \mathfrak{F}_1^n) :: \epsilon$, and $\rho = (\hat{a}_2^1, \tilde{p}_2^1, \mathbb{E}_2^1, \mathfrak{F}_2^1) :: \dots :: (\hat{a}_m^1, \tilde{p}_2^m, \mathbb{E}_2^m, \mathfrak{F}_2^m) :: \epsilon$, then for all $S \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} \mathfrak{o}$ $K$ and $S_j^i \xrightarrow{\nu|\hat{a}_j^i|\cdot|\tilde{p}_j^i|} \mathfrak{o}$ $K_j^i$, we have $(\rho @ \overrightarrow{S}_2)[(\pi @ \overrightarrow{S}_1)[\mathbb{E}[S]]] \xrightarrow{\tau} P'$.

3. if $P \xrightarrow{\mathbb{E}, \pi, \rho} \mathfrak{out} P'$, $\pi = (\hat{a}_1^1, \tilde{p}_1^1, \mathbb{E}_1^1, \mathfrak{F}_1^1) :: \dots :: (\hat{a}_n^1, \tilde{p}_1^n, \mathbb{E}_1^n, \mathfrak{F}_1^n) :: \epsilon$, and $\rho = (\hat{a}_2^1, \tilde{p}_2^1, \mathbb{E}_2^1, \mathfrak{F}_2^1) :: \dots :: (\hat{a}_m^1, \tilde{p}_2^m, \mathbb{E}_2^m, \mathfrak{F}_2^m) :: \epsilon$, then for all $S_j^i \xrightarrow{\nu|\hat{a}_j^i|\cdot|\tilde{p}_j^i|} \mathfrak{o}$ $K_j^i$, we have $(\rho @ \overrightarrow{S}_2)[(\pi @ \overrightarrow{S}_1)[\mathbb{E}[P]]] \xrightarrow{\tau} P'$.

Proof. The first item is by induction on the derivation of $R \xrightarrow{\mathbb{E},\rho} \mathfrak{P}'$. In the case of the rule inCom, we have $R = \xi \triangleright R''$, $\theta \in \xi \text{■}|\rho(\rho)|$, and $P' = \rho[\mathbb{R}''\theta[\mathbb{I}]]$. It is easy to check that $R \xrightarrow{|\rho(\rho)|} \mathfrak{o} R''\theta$, hence the result holds with $R' = R''\theta$. The inductive cases are straightforward.

The second and third items are proved by mutual induction on their deriva-
tion. The base cases are rules parInR and parInL; we handle the first one, the other
being symmetric. We have $\|R\::= \mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \epsilon, \rho} \mathfrak{par} P'$ with $R \xrightarrow{\bullet, (\hat{a}, \tilde{p}, \mathbb{E}, K \parallel) :: \rho} \mathfrak{in} P'$.
Let $\rho' = (\hat{a}, \tilde{p}, \mathbb{E}, K \parallel) :: \rho$. By the first item, there exists $R'$ such that $R \xrightarrow{|\rho(\rho')|} \mathfrak{o} R'$
and $P' = \rho'[\mathbb{R}']$. One can prove by induction on $\rho'$ that $(\rho' @ S \cdot \overrightarrow{S}_2)[R] \xrightarrow{\tau} P'$,
but $(\rho' @ S \cdot \overrightarrow{S}_2)[R] = (\rho @ \overrightarrow{S}_2)[\mathbb{E}[K \parallel R]]$, hence the result holds.

Most of the cases are straightforward by induction: parL, parR, parExtr, parNu,
outParL, outParR, and outNu. For outOut, we have $\bar{a}\langle M \rangle K \xrightarrow{\mathbb{E},\pi,\rho} \mathfrak{out} P'$ with
$\mathbb{E} \xrightarrow{K,(),(a,M),\pi,\rho} \mathfrak{par} P'$. Because $\bar{a}\langle M \rangle K \xrightarrow{\nu(),(a,M)} \mathfrak{o} K$, we have $(\rho @ \overrightarrow{S}_2)[\mathbb{E}[\bar{a}\langle M \rangle K]]] \xrightarrow{\tau} P'$ by the induction hypothesis, which is exactly what we
want.
For parOutR, we have $\|P\:: \mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \pi, \rho} \text{par} P'$ with $P \xrightarrow{\bullet, (\hat{a}, \tilde{p}, \mathbb{E}, K)} \text{out} P'$. Let $S \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} K$. We have $(\rho \otimes \vec{S}_2)[((\hat{a}, \tilde{p}, \mathbb{E}, K)] :: \pi \otimes S \cdot \vec{S}_1][P] \xrightarrow{\tau} P'$ by the induction hypothesis, but $(\rho \otimes \vec{S}_2)[((\hat{a}, \tilde{p}, \mathbb{E}, K)] :: \pi \otimes S \cdot \vec{S}_1][P] = (\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}_1)[\mathbb{E}[S \| P]]] = (\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}_1)[(\|P\:: \mathbb{E})[S]]],$ hence the result holds. The parOutL case is symmetric.

For parOutR$\rho$, we have $\|P\:: \mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \epsilon, \rho} \text{par} P'$ with $P \xrightarrow{\bullet, \epsilon, (\hat{a}, \tilde{p}, \mathbb{E}, K)} \text{out} P'$. Let $S \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} K$. We have $((\hat{a}, \tilde{p}, \mathbb{E}, K]) :: \rho \otimes S \cdot \vec{S}_2)[P] \xrightarrow{\tau} P'$ by the induction hypothesis, but $((\hat{a}, \tilde{p}, \mathbb{E}, K]) :: \rho \otimes S \cdot \vec{S}_2)[P] = (\rho \otimes \vec{S}_2)[\mathbb{E}[S \| P]] = (\rho \otimes \vec{S}_2)[(\|P\:: \mathbb{E})[S]],$ hence the result holds. The parOutL$\rho$ case is symmetric.

In the case of the parHoleL rule, we have $\bullet \xrightarrow{K_2, \hat{a}_2, \tilde{p}_2, (\hat{a}_1, \tilde{p}_1, \mathbb{E}, K_1)} \pi, \rho \xrightarrow{\bullet, \pi, \rho} \text{par} P'$ with $\mathbb{E} \xrightarrow{K_1 \parallel K_2, \hat{a}_1 \parallel \hat{a}_2, \tilde{p}_1 \parallel \tilde{p}_2, \pi, \rho} \text{par} P'$. Let $S \xrightarrow{\nu|\hat{a}_2|\cdot|\tilde{p}_2|} K_2$; then we deduce $S_1^1 \parallel S \xrightarrow{\nu|\hat{a}_1 \parallel \hat{a}_2|\cdot|\tilde{p}_2 \parallel \tilde{p}_2|} K_1 \parallel K_2$. Let $\vec{S}'_1$ such that $\vec{S}'_1 = S_1^1 \cdot \vec{S}'_1$. By induction, we have $(\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}'_1)[\mathbb{E}[S_1^1 \parallel S]]] \xrightarrow{\tau} P'$, but $(\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}'_1)[\mathbb{E}[S_1^1 \parallel S]]] = (\rho \otimes \vec{S}_2)[((\hat{a}_1, \tilde{p}_1, \mathbb{E}, K_1)] :: \pi \otimes S_1^1 \parallel \vec{S}'_1)[S] = (\rho \otimes \vec{S}'_2)[(\pi \otimes \vec{S}'_1)[\mathbb{E}[S_1^1 \parallel S]]] = (\rho \otimes \vec{S}_2)[((\hat{a}_1, \tilde{p}_1, \mathbb{E}, K_1)] :: \pi \otimes \vec{S}'_1)[S]$, as wished. The parHoleR case is symmetric.

**Lemma 7.** If $P \xrightarrow{\mathbb{E}, \pi, \rho} \text{out} P'$, then $\mathbb{E}[P] \xrightarrow{\bullet, \pi, \rho} \text{out} P'$.

*Proof.* By induction on $\mathbb{E}$.

**Lemma 8.** If $P \xrightarrow{\nu \vec{b} \cdot (a, M)} K$, then there exist $\mathbb{H}, \mathbb{G}$, and $K'$ such that $K = \mathbb{G}[K']$, $\mathbb{H} = \mathbb{G} \& \vec{b}^{-1}$, and $P = \mathbb{H}[\bar{a} \langle M \rangle K']$.

*Proof.* As in $\text{HO}\pi$.

**Lemma 9.** If $P \xrightarrow{\nu \vec{b} \cdot \vec{p}} K$ with $\text{sz}(\vec{p}) > 1$, then there exist $\mathbb{H}, \vec{a}, \hat{a}_1, \hat{a}_2, \tilde{p}_1, \tilde{p}_2, \mathbb{G}, P_1, P_2, K_1$, and $K_2$ such that $K = \mathbb{G}[K_1 \parallel K_2]$, $\vec{b} = |\vec{a} \cdot (\hat{a}_1 \parallel \hat{a}_2)|$, $\vec{p} = |\tilde{p}_1 \parallel \tilde{p}_2|$, $\mathbb{H} = \mathbb{G} \& \vec{a}^{-1}$, $P = \mathbb{H}[P_1 \parallel P_2]$, $P_1 \xrightarrow{\nu|\hat{a}_1|\cdot|\tilde{p}_1|} K_1$, and $P_2 \xrightarrow{\nu|\hat{a}_2|\cdot|\tilde{p}_2|} K_2$.

*Proof.* By induction on $P \xrightarrow{\nu \vec{b} \cdot \vec{p}} K$.

**Lemma 10.** If $\mathbb{E} \xrightarrow{\mathbb{G}[K], \vec{a} \cdot \hat{b}, \tilde{p}, \pi, \rho} \text{par} P'$, then for all $\mathbb{H} \in \mathbb{G} \& \vec{a}^{-1}$, we have $\mathbb{H}++\mathbb{E} \xrightarrow{K, \hat{b}, \tilde{p}, \pi, \rho} \text{par} P'$.

*Proof.* As in $\text{HO}\pi$.

**Lemma 11.** If $\mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \pi, \rho} \text{par} P'$ and $P \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} K$, then $\mathbb{E}[P] \xrightarrow{\bullet, \pi, \rho} \text{out} P'$.

*Proof.* We proceed by induction on $\text{sz}(|\tilde{p}|)$. If $\tilde{p} = (b, M)$, then $\hat{a} = \vec{a}$ and by Lemma 8. there exist $\mathbb{H}, \mathbb{G}$, and $K'$ such that $K = \mathbb{G}[K']$, $\mathbb{H} = \mathbb{G} \&$
For parOutR, we have $\|P\:: \mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \pi, \rho} \text{par} P'$ with $P \xrightarrow{\bullet, (\hat{a}, \tilde{p}, \mathbb{E}, K)} \xrightarrow{\pi, \rho} \text{out} P'$.
Let $S \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} \mathcal{O}$ $K$. We have $(\rho \otimes \vec{S}_2)[((\hat{a}, \tilde{p}, \mathbb{E}, K)] \:: \pi \otimes S \cdot \vec{S}_1][P] \xrightarrow{\tau} P'$ by the induction hypothesis, but $(\rho \otimes \vec{S}_2)[((\hat{a}, \tilde{p}, \mathbb{E}, K)] \:: \pi \otimes S \cdot \vec{S}_1][P] = (\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}_1)[\mathbb{E}[S \| P]]] = (\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}_1)[(\|P\:: \mathbb{E})[S]]],$ hence the result holds. The parOutL case is symmetric.

For parOutR$\rho$, we have $\|P\:: \mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \epsilon, \rho} \text{par} P'$ with $P \xrightarrow{\bullet, \epsilon, (\hat{a}, \tilde{p}, \mathbb{E}, K)} \xrightarrow{\rho} \text{out} P'$.
Let $S \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} \mathcal{O}$ $K$. We have $((\hat{a}, \tilde{p}, \mathbb{E}, K]) \:: \rho \otimes S \cdot \vec{S}_2][P] \xrightarrow{\tau} P'$ by the induction hypothesis, but $((\hat{a}, \tilde{p}, \mathbb{E}, K]) \:: \rho \otimes S \cdot \vec{S}_2][P] = (\rho \otimes \vec{S}_2)[\mathbb{E}[S \| P]] = (\rho \otimes \vec{S}_2)[(\|P\:: \mathbb{E})[S]],$ hence the result holds. The parOutL$\rho$ case is symmetric.

In the case of the parHoleL rule, we have $\bullet \xrightarrow{K_2, \hat{a}_2, \tilde{p}_2, (\hat{a}_1, \tilde{p}_1, \mathbb{E}, K_1)} \xrightarrow{\pi, \rho} \text{par} P'$ with $\mathbb{E} \xrightarrow{K_1 \parallel K_2, \hat{a}_1 \parallel \hat{a}_2, \tilde{p}_1 \parallel \tilde{p}_2, \pi, \rho} \text{par} P'$. Let $S \xrightarrow{\nu|\hat{a}_2|\cdot|\tilde{p}_2|} \mathcal{O}$ $K_2$; then we deduce $S_1^1 \parallel S \xrightarrow{\nu|\hat{a}_1 \parallel \hat{a}_2|\cdot|\tilde{p}_2 \parallel \tilde{p}_2|} \mathcal{O}$ $K_1 \parallel K_2$. Let $\vec{S}_1'$ such that $\vec{S}_1 = S_1^1 \cdot \vec{S}_1'$. By induction, we have $(\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}_1')][\mathbb{E}[S_1^1 \parallel S]]] \xrightarrow{\tau} P'$, but $(\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}_1')][\mathbb{E}[S_1^1 \parallel S]]] = (\rho \otimes \vec{S}_2)[((\hat{a}_1, \tilde{p}_1, \mathbb{E}, K_1]) \:: \pi \otimes S_1^1 \parallel \vec{S}_1')(S] = (\rho \otimes \vec{S}_2)[(\pi \otimes \vec{S}_1')(S][\mathbb{E}[S_1^1 \parallel S]]] = (\rho \otimes \vec{S}_2)[((\hat{a}_1, \tilde{p}_1, \mathbb{E}, K_1]) \:: \pi \otimes \vec{S}_1')(S]],$ as wished. The parHoleR case is symmetric.

**Lemma 7.** If $P \xrightarrow{\mathbb{E}, \pi, \rho} \text{out} P'$, then $\mathbb{E}[P] \xrightarrow{\bullet, \pi, \rho} \text{out} P'$.

*Proof.* By induction on $\mathbb{E}$.

**Lemma 8.** If $P \xrightarrow{\nu \vec{b} \cdot (a, M)} \mathcal{O}$ $K$, then there exist $\mathbb{H}, \mathbb{G}$, and $K'$ such that $K = \mathbb{G}[K']$, $\mathbb{H} = \mathbb{G} \& \vec{b}^{-1}$, and $P = \mathbb{H}[\bar{a} \langle M \rangle K']$.

*Proof.* As in $\text{HO}\pi$.

**Lemma 9.** If $P \xrightarrow{\nu \vec{b} \cdot \vec{p}} \mathcal{O}$ $K$ with $\text{sz}(\vec{p}) > 1$, then there exist $\mathbb{H}, \vec{a}, \hat{a}_1, \hat{a}_2, \tilde{p}_1, \tilde{p}_2, \mathbb{G}, P_1, P_2, K_1$, and $K_2$ such that $K = \mathbb{G}[K_1 \parallel K_2]$, $\vec{b} = |\vec{a} \cdot (\hat{a}_1 \parallel \hat{a}_2)|$, $\vec{p} = |\tilde{p}_1 \parallel \tilde{p}_2|$, $\mathbb{H} = \mathbb{G} \& \vec{a}^{-1}$, $P = \mathbb{H}[P_1 \parallel P_2]$, $P_1 \xrightarrow{\nu|\hat{a}_1|\cdot|\tilde{p}_1|} \mathcal{O}$ $K_1$, and $P_2 \xrightarrow{\nu|\hat{a}_2|\cdot|\tilde{p}_2|} \mathcal{O}$ $K_2$.

*Proof.* By induction on $P \xrightarrow{\nu \vec{b} \cdot \vec{p}} \mathcal{O}$ $K$.

**Lemma 10.** If $\mathbb{E} \xrightarrow{\mathbb{G}[K], \vec{a} \cdot \hat{b}, \tilde{p}, \pi, \rho} \text{par} P'$, then for all $\mathbb{H} \in \mathbb{G} \& \vec{a}^{-1}$, we have $\mathbb{H}++\mathbb{E} \xrightarrow{K, \hat{b}, \tilde{p}, \pi, \rho} \text{par} P'$.

*Proof.* As in $\text{HO}\pi$.

**Lemma 11.** If $\mathbb{E} \xrightarrow{K, \hat{a}, \tilde{p}, \pi, \rho} \text{par} P'$ and $P \xrightarrow{\nu|\hat{a}|\cdot|\tilde{p}|} \mathcal{O}$ $K$, then $\mathbb{E}[P] \xrightarrow{\bullet, \pi, \rho} \text{out} P'$.

*Proof.* We proceed by induction on $\text{sz}(|\tilde{p}|)$. If $\tilde{p} = (b, M)$, then $\hat{a} = \vec{a}$ and by Lemma 8. there exist $\mathbb{H}, \mathbb{G}$, and $K'$ such that $K = \mathbb{G}[K']$, $\mathbb{H} = \mathbb{G} \&$
$\vec{a}^{-1}$, and $P = \mathbb{H}[\overline{\mathfrak{b}\langle M \rangle K'}]$. We have $\mathbb{E} \xrightarrow{\mathbb{G}[K'], \vec{a}, (b,M), \pi, \rho} \text{par} P'$, which implies $\mathbb{H}++\mathbb{E} \xrightarrow{K', (), (b,M), \pi, \rho} \text{par} P'$ by Lemma 10. Applying rule outOut, we obtain $\overline{\mathfrak{b}\langle M \rangle K'} \xrightarrow{\mathbb{H}++\mathbb{E}, \pi, \rho} \text{out} P'$, and by Lemma 7, we get $(\mathbb{H}++\mathbb{E})[\overline{\mathfrak{b}\langle M \rangle K'}] \xrightarrow{\mathbb{H}++\mathbb{E}, \pi, \rho} \text{out} P'$. Because $(\mathbb{H}++\mathbb{E})[\overline{\mathfrak{b}\langle M \rangle K'}] = \mathbb{E}[\mathbb{H}[\overline{\mathfrak{b}\langle M \rangle K'}]] = \mathbb{E}[P]$, the result holds.

Suppose the result holds for $1 \le \text{sz}(\vec{p}) \le n-1$, and assume $\text{sz}(\vec{p}) = n$. By Lemma 9, there exist $\mathbb{H}, \vec{a}', |a_1|, |a_2|, \tilde{p}_1, \tilde{p}_2, \mathfrak{G}, P_1, P_2, K_1$, and $K_2$ such that $K = \mathbb{G}[K_1 \parallel K_2]$, $\hat{a} = \vec{a}' \cdot (|a_1| \parallel |a_2|)$, $\tilde{p} = \tilde{p}_1 \parallel \tilde{p}_2$, $\mathbb{H} = \mathfrak{G}$ & $\vec{a}'^{-1}$, $P = \mathbb{H}[P_1 \parallel P_2]$, $P_1 \xrightarrow{\nu|\hat{a}_1| \cdot |\tilde{p}_1|} K_1$, and $P_2 \xrightarrow{\nu|\hat{a}_2| \cdot |\tilde{p}_2|} K_2$. From $\mathbb{E} \xrightarrow{\mathbb{G}[K_1 \parallel K_2], \vec{a}' \cdot (\hat{a}_1 \parallel \hat{a}_2), \vec{p}_1 \parallel \vec{p}_2, \pi, \rho} \text{par} P'$, we deduce $\mathbb{H}++\mathbb{E} \xrightarrow{K_1 \parallel K_2, \hat{a}_1 \parallel \hat{a}_2, \vec{p}_1 \parallel \vec{p}_2, \pi, \rho} \text{par} P'$ by Lemma 10. Using rule parHoleL, we get $\bullet \xrightarrow{K_2, \hat{a}_2, \tilde{p}_2, (\hat{a}_1, \tilde{p}_1, \mathbb{H}++\mathbb{E}, K_1 \parallel) :: \pi, \rho} \text{par} P'$. By the induction hypothesis, we have $P_2 :: (\mathbb{H}++\mathbb{E}) \xrightarrow{K_1, \hat{a}_1, \tilde{p}_1, \pi, \rho} \text{par} P'$. With rule parOutR, we deduce $\parallel P_2 :: (\mathbb{H}++\mathbb{E}) \xrightarrow{\bullet, \pi, \rho} \text{out} P'$, and because $(\mathbb{H}++\mathbb{E})[P_1 \parallel P_2] = \mathbb{E}[\mathbb{H}[P_1 \parallel P_2]] = \mathbb{E}[P]$, the result holds.

**Lemma 12.** For all $P \xrightarrow{\vec{p}} \text{io} P'$, there exist $\rho, S_i \xrightarrow{\nu|\hat{a}_i| \cdot |\tilde{p}_i|} K_i$, and $R \xrightarrow{\cup_i |\tilde{p}_i| \cdot \vec{p}} \text{R'}$ such that $P = (\rho \oplus \vec{S})[R]$ and $P' = \rho[\vec{R'}]$.

*Proof.* By induction on $P \xrightarrow{\vec{p}} \text{io} P'$.

**Lemma 13.** For all $P \xrightarrow{\tau} P'$, there exist $\rho$ of size at least 1, $S_i \xrightarrow{\nu|\hat{a}_i| \cdot |\tilde{p}_i|} K_i$, and $R \xrightarrow{\cup_i |\tilde{p}_i|} \text{R'}$ such that $P = (\rho \oplus \vec{S})[R]$ and $P' = \rho[\vec{R'}]$.

*Proof.* By induction on $P \xrightarrow{\tau} P'$.

**Lemma 14.** For all $R \xrightarrow{\vec{p}} \text{R'}$, $\mathbb{E}$, and $\rho$, we have $R \xrightarrow{\mathbb{E}, \rho} \text{in} \rho[\mathbb{E}[\vec{R'}]]$.

*Proof.* By induction on $R \xrightarrow{\vec{p}} \text{R'}$.

**Theorem 8.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\tau} \text{zs} P'$.

*Proof.* By Lemma 13, there exist $\rho$ of size at least 1, $S_i \xrightarrow{\nu|\hat{a}_i| \cdot |\tilde{p}_i|} K_i$, and $R \xrightarrow{\cup_i |\tilde{p}_i|} \text{R'}$ such that $P = (\rho \oplus \vec{S})[R]$ and $P' = \rho[\vec{R'}]$. By Lemma 14, we have $R \xrightarrow{\bullet, \rho} \text{in} P'$. Because $\rho$ is of size at least 1, there exists $\rho'$ such that $\rho = (\hat{a}_1, \tilde{p}_1, \mathbb{E}_1, \tilde{\mathfrak{F}}_1) :: \rho'$. W.l.o.g., we assume $\tilde{\mathfrak{F}}_1 = K_1 \parallel$. By rule parlnR, we have then $\parallel R :: \mathbb{E}_1 \xrightarrow{K_1, \hat{a}_1, \tilde{p}_1, \epsilon, \rho'} \text{par} P'$. By Lemma 11, we have $\mathbb{E}_1[\mathbb{S}_1 \parallel R] \xrightarrow{\bullet, \epsilon, \rho'} \text{out} P'$.

For all $\rho'$, $Q \xrightarrow{\bullet, \epsilon, \rho'} \text{out} P'$, $\vec{K}, \vec{S}$ such that $S_i \xrightarrow{\nu|\hat{a}_i| \cdot |\tilde{p}_i|} K_i$, we prove as an intermediary result that $(\rho' \oplus \vec{S})[Q] \xrightarrow{\text{zs}} P'$ holds by induction on the size of $\rho'$. If $\rho'$ is empty, then we have in fact $Q \xrightarrow{\bullet, \epsilon, \epsilon} \text{out} P'$, and we conclude directly.
$\vec{a}^{-1}$, and $P = \mathbb{H}[\overline{b\langle M \rangle K'}]$. We have $\mathbb{E} \xrightarrow{\mathbb{G}[K'], \vec{a}, (b,M), \pi, \rho} \text{par} P'$, which implies $\mathbb{H}++\mathbb{E} \xrightarrow{K', (), (b,M), \pi, \rho} \text{par} P'$ by Lemma 10. Applying rule outOut, we obtain $\overline{b\langle M \rangle K'} \xrightarrow{\mathbb{H}++\mathbb{E}, \pi, \rho} \text{out} P'$, and by Lemma 7, we get $(\mathbb{H}++\mathbb{E})[\overline{b\langle M \rangle K'}] \xrightarrow{\mathbb{H}++\mathbb{E}, \pi, \rho} \text{out} P'$. Because $(\mathbb{H}++\mathbb{E})[\overline{b\langle M \rangle K'}] = \mathbb{E}[\mathbb{H}[\overline{b\langle M \rangle K'}]] = \mathbb{E}[P]$, the result holds.

Suppose the result holds for $1 \le \text{sz}(\vec{p}) \le n-1$, and assume $\text{sz}(\vec{p}) = n$. By Lemma 9, there exist $\mathbb{H}, \vec{a}', |a_1|, |a_2|, \tilde{p}_1, \tilde{p}_2, \mathbb{G}, P_1, P_2, K_1$, and $K_2$ such that $K = \mathbb{G}[K_1 \parallel K_2]$, $\hat{a} = \vec{a}' \cdot (|a_1| \parallel |a_2|)$, $\tilde{p} = \tilde{p}_1 \parallel \tilde{p}_2$, $\mathbb{H} = \mathbb{G}$ & $\vec{a}'^{-1}$, $P = \mathbb{H}[P_1 \parallel P_2]$, $P_1 \xrightarrow{\nu|\hat{a}_1|\cdot|\tilde{p}_1|} K_1$, and $P_2 \xrightarrow{\nu|\hat{a}_2|\cdot|\tilde{p}_2|} K_2$. From $\mathbb{E} \xrightarrow{\mathbb{G}[K_1 \parallel K_2], \vec{a}' \cdot (\hat{a}_1 \parallel \hat{a}_2), \vec{p}_1 \parallel \vec{p}_2, \pi, \rho} \text{par} P'$, we deduce $\mathbb{H}++\mathbb{E} \xrightarrow{K_1 \parallel K_2, \hat{a}_1 \parallel \hat{a}_2, \vec{p}_1 \parallel \vec{p}_2, \pi, \rho} \text{par} P'$ by Lemma 10. Using rule parHoleL, we get $\bullet \xrightarrow{K_2, \hat{a}_2, \tilde{p}_2, (\hat{a}_1, \tilde{p}_1, \mathbb{H}++\mathbb{E}, K_1 \parallel) :: \pi, \rho} \text{par} P'$. By the induction hypothesis, we have $P_2 :: (\mathbb{H}++\mathbb{E}) \xrightarrow{\bullet, (\hat{a}_1, \tilde{p}_1, \mathbb{H}++\mathbb{E}, K_1 \parallel) :: \pi, \rho} \text{out} P'$; with rule parOutR, we deduce $\parallel P_2 :: (\mathbb{H}++\mathbb{E}) \xrightarrow{K_1, \hat{a}_1, \tilde{p}_1, \pi, \rho} \text{par} P'$. By the induction hypothesis, we have $(\mathbb{H}++\mathbb{E})[P_1 \parallel P_2] \xrightarrow{\bullet, \pi, \rho} \text{out} P'$, and because $(\mathbb{H}++\mathbb{E})[P_1 \parallel P_2] = \mathbb{E}[\mathbb{H}[P_1 \parallel P_2]] = \mathbb{E}[P]$, the result holds.

**Lemma 12.** For all $P \xrightarrow{\vec{p}} \text{io} P'$, there exist $\rho, S_i \xrightarrow{\nu|\hat{a}_i|\cdot|\tilde{p}_i|} K_i$, and $R \xrightarrow{\cup_i|\tilde{p}_i|} \text{R}'$ such that $P = (\rho \oplus \vec{S})[R]$ and $P' = \rho[\text{R}']$.

*Proof.* By induction on $P \xrightarrow{\vec{p}} \text{io} P'$.

**Lemma 13.** For all $P \xrightarrow{\tau} P'$, there exist $\rho$ of size at least 1, $S_i \xrightarrow{\nu|\hat{a}_i|\cdot|\tilde{p}_i|} K_i$, and $R \xrightarrow{\cup_i|\tilde{p}_i|} \text{R}'$ such that $P = (\rho \oplus \vec{S})[R]$ and $P' = \rho[\text{R}']$.

*Proof.* By induction on $P \xrightarrow{\tau} P'$.

**Lemma 14.** For all $R \xrightarrow{\vec{p}} \text{R}'$, $\mathbb{E}$, and $\rho$, we have $R \xrightarrow{\mathbb{E}, \rho} \text{in} \rho[\mathbb{E}[\text{R}']]$.

*Proof.* By induction on $R \xrightarrow{\vec{p}} \text{R}'$.

**Theorem 8.** If $P \xrightarrow{\tau} P'$, then $P \xrightarrow{\tau} \text{zs} P'$.

*Proof.* By Lemma 13, there exist $\rho$ of size at least 1, $S_i \xrightarrow{\nu|\hat{a}_i|\cdot|\tilde{p}_i|} K_i$, and $R \xrightarrow{\cup_i|\tilde{p}_i|} \text{R}'$ such that $P = (\rho \oplus \vec{S})[R]$ and $P' = \rho[\text{R}']$. By Lemma 14, we have $R \xrightarrow{\bullet, \rho} \text{in} P'$. Because $\rho$ is of size at least 1, there exists $\rho'$ such that $\rho = (\hat{a}_1, \tilde{p}_1, \mathbb{E}_1, \mathfrak{F}_1) :: \rho'$. W.l.o.g., we assume $\mathfrak{F}_1 = K_1 \parallel$. By rule parlnR, we have then $\parallel R :: \mathbb{E}_1 \xrightarrow{K_1, \hat{a}_1, \tilde{p}_1, \epsilon, \rho'} \text{par} P'$. By Lemma 11, we have $\mathbb{E}_1[\mathbb{S}_1 \parallel R] \xrightarrow{\bullet, \epsilon, \rho'} \text{out} P'$.

For all $\rho'$, $Q \xrightarrow{\bullet, \epsilon, \rho'} \text{out} P'$, $\vec{K}, \vec{S}$ such that $S_i \xrightarrow{\nu|\hat{a}_i|\cdot|\tilde{p}_i|} K_i$, we prove as an intermediary result that $(\rho' \oplus \vec{S})[Q] \xrightarrow{\text{zs}} P'$ holds by induction on the size of $\rho'$. If $\rho'$ is empty, then we have in fact $Q \xrightarrow{\bullet, \epsilon, \epsilon} \text{out} P'$, and we conclude directly.
Otherwise, there exists $\rho''$ such that $\rho' = (\hat{a}_2, \tilde{p}_2, \mathbb{E}_2, \mathfrak{F}_2) :: \rho''$. W.l.o.g., we assume $\mathfrak{F}_2 = K_2 \| \cdot$ By rule parOutR$\rho$, we have then $\|Q :: \mathbb{E}_2 \xrightarrow{K_2, \hat{a}_2, \tilde{p}_2, \epsilon, \rho''} \mathrm{par} P'$. By Lemma 11, we have $\mathbb{E}_2[\|S_2 \| Q] \xrightarrow{\bullet, \epsilon, \rho'} \mathrm{out} P'$. Let $\vec{S}'$ such that $\vec{S} = S_2 \cdot \vec{S}'$ By the induction hypothesis, we have $(\rho'' @ \vec{S}')[\mathbb{E}_2[\|S_2 \| Q]] \to_{\mathrm{zs}} P'$, i.e., $\rho'[\vec{S}]Q \to_{\mathrm{zs}} P'$, as wished.

Let $\vec{S}'$ such that $\vec{S} = S_1 \cdot \vec{S}'$. From the intermediary result, we deduce $(\rho' @ \vec{S}')[\mathbb{E}_1[\|S_1 \| R]] \to_{\mathrm{zs}} P'$, but $(\rho' @ \vec{S}')[\mathbb{E}_1[\|S_1 \| R]] = (\rho @ \vec{S})[R] = P$, hence the result holds.
Otherwise, there exists $\rho''$ such that $\rho' = (\hat{a}_2, \tilde{p}_2, \mathbb{E}_2, \mathfrak{F}_2) :: \rho''$. W.l.o.g., we assume $\mathfrak{F}_2 = K_2 \| \cdot$ By rule parOutR$\rho$, we have then $\|Q :: \mathbb{E}_2 \xrightarrow{K_2, \hat{a}_2, \tilde{p}_2, \epsilon, \rho''} \mathrm{par} P'$. By Lemma 11, we have $\mathbb{E}_2[\|S_2 \| Q] \xrightarrow{\bullet, \epsilon, \rho'} \mathrm{out} P'$. Let $\vec{S}'$ such that $\vec{S} = S_2 \cdot \vec{S}'$ By the induction hypothesis, we have $(\rho'' @ \vec{S}')[\mathbb{E}_2[\|S_2 \| Q]] \to_{\mathrm{zs}} P'$, i.e., $\rho'[\vec{S}]Q \to_{\mathrm{zs}} P'$, as wished.

Let $\vec{S}'$ such that $\vec{S} = S_1 \cdot \vec{S}'$. From the intermediary result, we deduce $(\rho' @ \vec{S}')[\mathbb{E}_1[\|S_1 \| R]] \to_{\mathrm{zs}} P'$, but $(\rho' @ \vec{S}')[\mathbb{E}_1[\|S_1 \| R]] = (\rho @ \vec{S})[R] = P$, hence the result holds.