# First-order store and visibility in name-passing calculi

Daniel Hirschkoff

Iwan Quémerais

Davide Sangiorgi

## Abstract

The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store.

We study how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed.

# 1 Introduction

The π-calculus is one of the best known process calculi. It has a handful of operators — parallelism, input, output, restriction being the main ones — with which it achieves an amazing expressive power. Yet, it has a rich algebraic theory and a wide spectrum of proof techniques. In the π-calculus, computation is communication, by means of message-passing synchronisations between processes. Names are the communication units; new names may be created, and may themselves be exchanged in communications. When used for modelling, π-calculus is normally typed, so to be able to support structured data values, beginning with basic first-order values such as integers and booleans.

The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. For instance, the representation of functions as π-calculus processes has been widely studied, beginning with Milner's seminal work [14]. Usually, higher-order languages include forms of store. It is therefore important to understand how expected semantic properties of store can be captured in a language for pure concurrency such as the π-calculus.

An aspect of store with strong semantic consequences is the distinction between higher-order and first-order store. The term 'first-order store' refers to a memory model where variables can hold only basic data types such as integers and booleans. This contrasts with a higher-order store, where variables can also store functions, or code, or references to these. Limiting the store to first-order data makes it easier to reason about program behaviours, and verify behavioural properties. It may also enhance security and predictability guarantees by preventing unintended behaviours associated with dynamic function storage and code
injection. A striking example of a property that may be broken with higher-order store is termination. For instance, the simply-typed λ-calculus is strongly normalising and therefore terminating. This property is maintained by the addition of first-order store, but not with higher-order store, as functions may recursively reference and invoke each other through the store. In game semantics of higher-order languages, the distinction between first-order and higher-order store has led to studying the concept of visibility. Intuitively, visibility ensures us that each move in a computational game is justified by prior interactions. With the introduction of higher-order store, the visibility condition has to be relaxed, reflecting the added complexity in tracking information flow within a program.

The goal of this paper is precisely to understand the meaning of first-order store and visibility within the π-calculus. In functional languages based on the λ-calculus, imposing first-order store is simply determined by the constraint that all references may only store first-order values. In the π-calculus, in contrast, there is no explicit notion of reference, and therefore the meaning of ‘first-order store’ requires some care. In π-calculi, a piece of store is usually represented by an output message. For instance $\overline{h}\langle 5 \rangle$ may be thought of as the statement that name h currently contains 5. A process that inputs at h and then re-emits a message at h, such as $h(z)$. $\overline{h}\langle z+1 \rangle$, is a process that acts on such a store. In this case, h is a first-order name, hence h implements a piece of first-order store. An example of higher-order store is given by the process

$$P \stackrel{\text{def}}{=} a(b). ((\overline{b}(d)).!d.R) \mid c.\overline{b}(d').d'.R') \quad (1)$$

Here, $\overline{b}(d)$ is a bound output, and represents the output of a ‘new’ name d, and similarly for $\overline{b}(d')$; whereas, e.g., $d.R$ and $c.Q$ represent inputs in which no value is exchanged (i.e., $d$ and $c$ carry unit values). In $P$, name $a$ is higher-order, in that $a$ carries a (pointer to a) service. In the input at $a$, the service name received in the input (the parameter $b$) is used after the input, but it is also stored, and used later when $c$ is invoked. In other words, the visibility of $c$ (the services that $c$ may call when invoked) depends on interactions that have occurred earlier, at $a$. For this reason, $P$ implements a form of higher-order store. When this does not happen, that is, the visibility of a higher-order name (the set of services that may be called when the name is invoked) may be determined at the point in which the name is created, the process implements a form of first-order store. (The word ‘service’ is freely used, here and elsewhere, to indicate the input end of a name; in π-calculus, a name may have multiple input occurrences, in arbitrary syntactic positions within a process, in contrast with, say, the function declarations in functional languages, which are supposed to be unique.)

The amazing expressive power of the π-calculus also makes the contexts of the calculus very discriminating; as a consequence, behavioural equivalences, which are supposed to be preserved by the contexts of the calculus, are rather demanding relations. A well-established way of imposing constraints on the set of legal contexts, thus obtaining usefully coarser behavioural equivalences, is to adopt behavioural type systems. Types may be used in order to capture communication patterns on the usage of names, such as capabilities, linearity, sessions, and so on, e.g., [18, 10, 5, 1]. Type systems have also been designed to capture specific properties of processes, such as termination, deadlock-freedom, lock-freedom, e.g., [23, 11, 17].
A further step is then to tune the proof techniques of the π-calculus to such type systems, so to be able to actually prove the behavioural equalities that only hold in presence of types. For instance, in the case of may testing (or contextual equivalence) this may yield to refinements or modifications of the notion of trace equivalence; whereas in the case of barbed equivalence this may lead to refinements or modifications of the standard notion of labelled bisimilarity. The resulting proof techniques must be sound with respect to initial contextually-defined relations; ideally, they should also be complete.

In this paper we propose a type system that guarantees first-order store in π-calculus processes. The type system makes use of visibility functions, that is, partial finite functions that specify, for each higher-order name b that may occur free in a process, the set of services (i.e., higher-order names) that may be invoked when a call at b is made. In order to better understand the behavioural effects of visibility, we combine it first with sequentia lity and then with well-bracketing. ‘Sequentiality’ intuitively indicates the existence of a single thread of computation. That is, at any point there is a single process that is active and decides what the next computation step can be. In the encodings of the λ-calculus [15, 20], a process is active, i.e., it carries the thread, when it contains an unguarded output at a higher-order name. When encoding λ-calculi with first-order references, an active process may also expose the thread by exhibiting an input at a first-order name. We follow such a convention also in the paper: higher-order names carry the thread via outputs, first-order names via inputs (other choices technically would however be possible). Sequentiality allows us to expose, in isolation, the causality properties of service calls, within a standard (interleaving) semantics. These aspects would be partially or totally obscured by the presence of other concurrent threads.

In higher-order languages, the effects of having first-order store are particularly strong in absence of control operators; that is, using a terminology borrowed from game semantics, in a 'well-bracketed' setting, where the call-return interaction behaviour between a term and its context follows a stack discipline. We therefore also consider the refinement of our visibility-based type system under the well-bracketing hypothesis. To see an example of the effect of visibility, consider the following well-bracketed example:

$$ \nu h (\bar{h}\langle 0 \rangle \mid \bar{a}(c, q). (!c. h(z). \bar{h}\langle z+1 \rangle \mid q(y). Q)) $$

Here, an external service a is called, exporting a local service c capable of incrementing a private reference h, and with a return channel q. If visibility holds, then the external environment cannot store c. Therefore, after providing an answer at q, the environment is unable to call c again, thus incrementing h, unless an access to c is explicitly provided again (by process Q). This property may be used to perform optimisations, possibly including garbage-collection of the service c if at some point c is not used anymore in Q.

We then study characterisations for both may testing and barbed equivalence, as special forms of trace equivalence and of labelled bisimilarity. Following the tradition of testing, the language includes special success signals, that are used by testers (i.e, processes running in parallel with the testees), and may be used at any time, to report success.

When developing such characterisations, some care is necessary so to distinguish between the visibility of the tested and of the tester processes, as they need not be the same. For this,
we introduce visibility-constrained LTSs, in which process transitions are constrained by a
visibility function, intuitively expressing the possibility for processes to perform a certain
transition given a certain visibility function for the external observer. As a consequence of the
transition, the visibility function may need to be updated, so to yield the visibility function
for the next transition. In the case of well-bracketing, the constraints given by visibility have
to be coupled with those given by the stack names used to track well-bracketing (and again,
a distinction has to be made between the stacks for the testers and those for the testees).
Based on these LTSs, we introduce forms of trace equivalence and of labelled bisimilarity
that are proved to be sound and complete, for may testing and barbed equivalence, both in
the case of sequentiality and in that of well-bracketing.

We present the version of the π-calculus with higher-order and first-order names in Section 2. In Section 3, we define the type system implementing visibility for sequential processes. We define typed labelled transitions and present labelled characterisations of behavioural equivalences in Section 4. Section 5 is devoted to the extension with well-bracketing.

## 2 Background: the π-calculus language

The π-calculus language that will be used is called, technically, Internal π (πI) [21] (all channels exchanged are fresh – no free object outputs), with the addition of *first-order values* (such as integers and booleans), and expressions that evaluate to first-order values, called *first-order expressions*. We do not specify what exactly first-order values and first-order expressions are. We simply assume that, in a closed process, a first-order expression evaluates to a first-order value. Moreover, only the output capability of names may be exported. This means that, for instance, in an input *a(b)*. *P* name *b* may only be used in output in *P*. This constraint is often followed in theory and applications of the π-calculus, as it simplifies various technical matters.

We assume that names are distinguished (partitioned) into *higher-order* names and *first-order* names, and *success names*. Higher-order names are the ordinary πI names; first-order names may only carry first-order values, and they may not be passed around (the second constraint simplifies the technical details, though it is not mandatory, see Section 3). In later sections, first-order names will be used to represent references. The fact that these names may only carry first-order values, together with constraints on visibility, will ensure that the calculus does not have (implicit or explicit forms of) higher-order store. The *success names* are used, in the tradition of testing equivalences, by tester processes so to report results of experiments on tested processes (thus, the processes compared in the examples of the paper do not contain success names).

The calculi in the paper will be typed. For simplicity we define our type systems as refinements of the most basic type system for π-calculus, namely Milner’s *sorting* [13], in which names are partitioned into a collection of *types* (or sorts), and a sorting function maps types onto types. We assume that there is a sorting system under which all processes we manipulate are well-typed. Thus, the sorting system separates higher-order and first-order
<figure><img src="image_1.png" /><figcaption>Table 1: The syntax of the calculus</figcaption></figure>

names; moreover we assume that first-order names are monadic, and that higher-order names carry a pair of a first-order value and a higher-order name. Thus $\bar{a}\langle v \rangle(b)$. $P$ is the output of the first-order value $v$ and of the fresh higher-order name $b$ at the (higher-order) name $a$, with continuation $P$. When writing examples, we allow different sortings; for instance, writing $a.P$ and $\bar{b}.Q$ for inputs and outputs in which no value is exchanged.

The syntactic categories of the calculus are presented in Table 1. As usual, input and restriction are binding constructs, and give rise to the expected definitions of free and bound names. An expression or a process is closed if it does not have free (first-order) variables. It is intended that transitions are defined on closed processes.

The definition of structural congruence, written $\equiv$, and of the strong and weak (untyped) labelled transitions, written $\xrightarrow{\mu}$, $\Rightarrow$, and $\stackrel{\hat{\mu}}{\Rightarrow}$, are standard and are given in Appendix A (later we will introduce typed variants of the LTS). We note $\mathit{fn}(P)$ (resp. $\mathit{fn}(\mu)$) the set of free names of $P$ (resp. $\mu$). We sometimes abbreviate reductions $P \xrightarrow{\tau} P'$ as $P \rightarrow P'$.

As behavioural equivalences we consider both may-testing and barbed equivalence. Both relations are contextual, in that they are defined by requiring a closure under all 'observers'. They both use 'barbs' (or 'success') signals; barbed equivalence, in addition, makes use of a bisimulation game on reductions. We write $\downarrow_{\omega}$ to indicate the possibility of exhibiting an $\omega$ barb, possibly after some reductions; i.e., $P \downarrow_{\omega}$ holds if there is $P'$ with $P \Rightarrow P'$ and $P'$ has an unguarded occurrence of $\omega$. Thus intuitively two processes are behaviourally equal if they can produce 'the same barbs' under all legal observers running in parallel with them. As we are in a typed setting, observer and tested processes should have compatible typings. The meaning of 'compatible' depends on the specific type system. For visibility, the meaning will be specified in Sections 3 and 5. We write $\Delta \vdash P$, and say that $P$ is a $\Delta$-process, if $P$ is typable under $\Delta$, and $\Delta \vdash P, Q$ if both $\Delta \vdash P$ and $\Delta \vdash Q$ hold. Behavioural equivalences are defined on closed processes; they are extended to open processes (i.e., processes with free first-order variables) in the usual manner, by considering all possible closing substitutions. We only consider weak behavioural equivalences (i.e., equivalences that abstract from internal moves of processes, the reductions), as these are, in practice, the most useful ones.

**Definition 1** (May testing). Suppose that $\Gamma, \Delta$ are compatible. Then two $\Delta$-processes $P$ and $Q$ are may testing equivalent at $\Gamma$, written $P \cong_{\Delta}^{\Gamma} Q$, if for all $R$-processes and success name $\omega$, we have $(R|P) \downarrow_{\omega}$ iff $(R|Q) \downarrow_{\omega}$.
**Definition 2** (Barbed bisimilarity and equivalence). *Barbed bisimilarity* is the largest symmetric relation $\approx$ s.t. $P \approx Q$ implies:

1. whenever $P \to P'$, there exists $Q'$ such that $Q \implies Q'$ and $P' \approx Q'$;

2. for each $\omega$, if $P \downarrow_{\omega}$ then also $Q \downarrow_{\omega}$.

Suppose that $\Gamma, \Delta$ are compatible. Then two $\Delta$-processes $P$ and $Q$ are *barbed equivalent at* $\Gamma$, written $P \cong_{\Gamma}^{\Delta} Q$, if for all $R$ with $\Gamma \vdash R$ it holds that $P | R \approx Q | R$.

We write $P \cong Q$ (resp. $P \cong Q$) when $P \cong_{\Gamma}^{\Delta} Q$ (resp. $P \cong_{\Delta}^{\Gamma} Q$) holds under any typing $\Delta$ for $P, Q$ and any $\Gamma$ compatible with $\Delta$.

We now introduce some notations that will be useful below. In the paper we use partial functions whose codomains are finite powersets. If $\Delta$ is such a function, then $\Delta; i \mapsto A$ is the extension of $\Delta$ in which $i$ is mapped onto $A$, assuming that $i$ is not in $\text{dom}(\Delta)$; conversely $\Delta^{-i}$ is the restriction of $\Delta$ in which the entry for $i$ is erased, both in the domain and codomain of $\Delta$. We also write $i \mapsto A, j$ as an abbreviation for $i \mapsto (A \cup \{j\})$; and $\Delta \downarrow i$ (resp. $\Delta \nrightarrow i$) means that $\Delta$ is (resp. is not) defined on $i$. Function $\Delta_1 \cap \Delta_2$ has domain $\text{dom}(\Delta_1) \cap \text{dom}(\Delta_2)$, and then is defined as $(\Delta_1 \cap \Delta_2)(p) = \Delta_1(p) \cap \Delta_2(p)$; and likewise for $\Delta_1 \cup \Delta_2$. We write $\Delta_1 \subseteq \Delta_2$ if $\text{dom}(\Delta_1) \subseteq \text{dom}(\Delta_2)$, and for each $i \in \text{dom}(\Delta_1)$, we have $\Delta_1(i) \subseteq \Delta_1(i)$.

## 3 A Type System for Visibility

Our type system for visibility is built on top of that for sequentiality [3]. While visibility could be defined as a standalone notion, the combination with sequentiality makes the behavioural effects sharper and easier to grasp.

Intuitively, sequentiality ensures us that at any time at most one interaction can occur; i.e., there is a single computation thread. A process that holds the thread, called *active*, decides what the next interaction can be. It does so by offering a single particle (input or output) that controls the thread. A given name may exercise the control on the thread either in output or in input. Following [3], we require that, in higher-order names, the thread is carried by outputs, whereas, in first-order names, it is carried by inputs. An input that carries the thread maintains the thread, whereas an output releases it. (These appear to be, practically, the most interesting combinations; other combinations could be adopted, with the expected modifications.) Thus, for instance, the following process $P$ is well-typed:

$$P \stackrel{\text{def}}{=} (h(x). \bar{a}\langle x \rangle(b). (b(z, c'). Q | \bar{h}\langle x \rangle)) | \bar{k}\langle v \rangle$$

The initial particles in $P$ are the input at $h$ and the output at $k$; however only the input at $h$ carries the thread, as $h$ and $k$ are first-order. Underneath the input, the thread is maintained and released in the output at $a$ (the thread will be acquired by the process in the external environment performing the input at $a$); later, when the input at $b$ is performed, process $Q$ obtains the thread back. Sequentiality however does not exclude non-determinism: e.g., an output particle may have the possibility of interacting with different inputs.
The type system for visibility intuitively allows us to specify which possible higher-order outputs can be performed by a process that becomes active. Type environments are partial functions, called visibility functions, acting on higher-order names and, for active processes, on the special token *, representing the active thread. (Later, when studying well-bracketing, type environments will have both a visibility function and a name stack.)

**Definition 3 (Visibility function).** A visibility function is a finite partial function $\Delta : HO \cup \{\ast\} \to P_{fin}(HO)$. Moreover the function should be transitive, that is, for all $o \in dom(\Delta)$, if $\Delta \searrow a$ and $a \in \Delta(o)$, then $\Delta(a) \subseteq \Delta(o)$.

To see the use of *, suppose $\Delta(\ast) = \{a, b\}$; this means that a $\Delta$-process is active, and may only perform outputs at $a$ and $b$, as in the following process:

$$ \bar{a}\langle v \rangle(c). c(d). \bar{b}(w). \mathbf{0} $$

Name $c$ is created in the output at $a$ and therefore $c$ inherits $a$'s visibility.

Similarly, if $\Delta(d) = \{a, b\}$ then, in a $\Delta$-process $d(x, c)$. $P$, the continuation $P$ of the input at $d$ may only perform outputs at $a$, $b$ or at $c$ (as $c$ is the higher-order name received in the input). The use of visibility functions also allows us to sort out implicit form of higher order store; in the following example, $p, q$ are higher order names used for continuations.

**Example 4 (Implicit forms of higher-order store).** In the $\lambda$-calculus, if a term without higher-order references is well-bracketed then it necessarily obeys visibility. In our calculus, even though we do not have explicit higher-order references, we can simulate higher-order store. Consider

$$ P \stackrel{\text{def}}{=} \bar{a}(b, p). b(n, c, q). \bar{q}\langle n \rangle. p(m). \bar{c}. \mathbf{0} $$

In $P$ the visibility $\Delta(p)$ is defined when the output at $a$ is made, therefore $c \notin \Delta(p)$, and the final output at $c$ breaks visibility; indeed, the input at $b$, which justifies the output at $c$, is answered by the output at $q$ before the output at $c$.

Transitivity ensures us that the visibility functions, viewed as ‘named sets’, represent transitive sets. Transitivity is needed to guarantee the behavioural expectations of visibility. If a process $P$ calls a service $a$, with actual (higher-order) parameter $b$, then an output triggered by such a call (and possibly directed back to $P$) should be either at $b$ or at a name in the visibility of $a$; however, the server $a$ might call an external service $c$; this call should not allow an increase of the visibility associated to $a$; hence the transitivity constraint that the visibility of $c$ is contained in that of $a$. Technically, transitivity is necessary to ensure preservation of typing under reduction (see Theorem 10 and Example 11).

**Remark 5 (Transitivity and functional languages).** The issue of transitivity does not arise in the semantics of purely functional languages such as the $\lambda$-calculus [6]: visibility functions do appear, but the domain and codomain of such functions are disjoint (technically, in the game semantics terminology, the domain contains names introduced by Player, whereas the codomain contains names introduced by Opponent). This makes transitivity trivial.
<figure><img src="image_2.png" /><figcaption>Figure 1: Typing rules for visibility</figcaption></figure>

In the typing of a parallel composition, the visibility function has to be split between the two components of the composition. This is important for elements of the domain of the function that are linear, and therefore may only appear in one, but not both, components; this is the case for *, and the linear continuation names that will be introduced in Section 5.

**Definition 6 (Split).** Let $\Delta$ be a visibility function, we define $\mathit{split}(\Delta)$ as the set of pairs $(\Delta_1, \Delta_2)$ such that $\Delta_1 \cup \Delta_2 = \Delta$ and $* \notin \mathit{dom}(\Delta_1) \cap \mathit{dom}(\Delta_2)$.

The typing rules are given in Table 1. We comment on a few of them. Rule O-HO specifies that an output at a HO name $a$ owns the thread, and that name $a$ must be in the current visibility. In the continuation $P$ (which is not active) the visibility for $b$ is determined by the current visibility $\Delta(*)$ together with $b$ itself, to allow for recursive calls at $b$. Symmetrically, in rule I-HO, a process performing an input at $a$ acquires the thread, with a visibility given by $\Delta(a)$ plus the received name $b$. A replicated input is well-typed only if it is not active (rule REP). When typing parallel composition, we use split to insure that at most one of the components holds the thread. We simply remove the name from $\Delta$ when typing a restriction (rule RES-HO). Visibility plays no role in rules I-FO and O-FO; the only checks made are given by sequentiality, concerning the respect of the thread.

**Example 7.** Consider

$$ P \stackrel{\text{def}}{=} \begin{array}{@{}l@{}} a(x, b). \bar{b}\langle x + 1 \rangle(d). a(x', b'). \bar{b}\langle x + x' \rangle(d'). \mathbf{0} \\ \mid \quad a(x_1, b_1). \bar{b}_1\langle x_1 \rangle(d_1). d_1(d_2). \bar{c}\langle x + 1 \rangle(c_1). \mathbf{0} \end{array} $$

The process has three inputs at $a$; the first two are sequential, and make no requirements on visibility, as their continuations only perform outputs at names received in the input; the third one, in addition, has the effect of creating a name $d_1$, whose input may activate an output at the free name $c$. This input requires that in the visibility $\Delta$ of $P$, we find $c \in \Delta(a)$.
**Example 8.** (In this example, we ignore the first-order components of actions, as they are not relevant.) A process of the form

$$P \stackrel{\text{def}}{=} \bar{a}(b). (Q \mid c(d). \bar{b}(d'). R)$$

is not typable: the initial visibility of $c$ may not include $b$, which is created fresh by $a$; yet, $P$ may perform an output at $b$ after the input at $c$. Indeed, while $P$ does not directly create a form of higher-order store, it may do so indirectly: the external environment, after completing the treatment of the initial call at $a$, is supposed to ‘forget’ the higher-order name $b$. However, this is not the case, as the environment may regain access to $b$ by invoking the (unrelated) name $c$. In contrast $P$ would become typable (in the straightforward extension of our type system with polyadicity) if the initial output at $a$ would be replaced by $\bar{a}(b, c)$: now $c$ becomes a fresh name, initially unknown, and created in the initial output, together with $b$, so that the visibility for $b$ and $c$ can be the same and can include both names.

The following lemma shows that a visibility function may always be enlarged (both in the domain and codomain), as long as sequentiality (i.e., being defined on $*$) is respected.

**Lemma 9 (Weakening).** Suppose $\Delta_1 \vdash P$, $\Delta_1 \subseteq \Delta_2$, and $(\Delta_2 \searrow * \iff \Delta_1 \searrow *)$. Then $\Delta_2 \vdash P$.

Some other technical lemmas that are used in proofs are presented in Appendix B.1.

**Theorem 10 (Subject reduction).** Suppose $\Delta \vdash P$ and $P \stackrel{\mu}{\to} P'$. We have:

* if $\mu$ is a $\tau$ action or a first-order input, then $\Delta \vdash P'$; the same holds if $\mu$ is a first-order output and $\Delta \nvdash *$;

* if $\mu = \bar{a}\langle v \rangle(b)$ then $a \in \Delta(*)$ and $\Delta^{-*}; b \mapsto \Delta(*)$, $b \vdash P'$;

* if $\mu = a\langle v \rangle(b)$ and $\Delta \nvdash *$, then $\Delta; * \mapsto \Delta(a), b \vdash P'$.

**Example 11.** Transitivity of visibility functions is necessary. Indeed, consider process $P \stackrel{\text{def}}{=} a. \bar{b}. Q \mid \bar{a}$, and the non-transitive function $\Delta = a \mapsto \{a, b\}, * \mapsto a$. We have $\Delta \vdash P$. However $P \stackrel{\tau}{\to} \bar{b}. Q$, with $\Delta \nvdash \bar{b}. Q$, violating Subject Reduction (Theorem 10).

To adapt the generic definitions of behavioural equivalence in Section 2 to the type system for visibility, we only have to specify the meaning of compatibility between typing environments (which in our case are visibility functions). Compatibility means ensuring that processes typed under the two typing environments cannot both be active.

**Definition 12.** Two typings $\Delta_1$ and $\Delta_2$ are compatible if $* \notin \text{dom}(\Delta_1) \cap \text{dom}(\Delta_2)$.

We discuss some examples of equivalences in which the behavioural constraints imposed on legal observers by visibility are essential: the equivalences would otherwise be broken.
**Example 13.** Consider a process

$$P \stackrel{\text{def}}{=} \bar{a}(b, c) \cdot P' \quad \text{for} \quad P' \stackrel{\text{def}}{=} (b(d) \cdot R) \mid c(c_1) \cdot \bar{a}(b', c') \cdot c'(c_2) \cdot \bar{b}(d') \cdot Q$$

where we assume $b$ does not occur in $Q$ and $R$. Process $P$ interrogates an external service $a$, providing access to local services $b$ and $c$, and the derivative is $P'$. Now, $P'$ may either be interrogated at $b$, or at $c$. In the former case, the output $\bar{b}(d')$. $Q$ becomes dead code (as the environment may not install any input at $b$). In the latter case, the environment is again called at $a$; now, since visibility ensures us the environment cannot remember $b$, the input and the output at $b$ in $P'$ may only interact with each other; we can therefore inline the call at $b$. We can express this behaviour using expansion as follows:

$$P \cong \bar{a}(b, c) \cdot \left( \begin{array}{l} b(d) \cdot (R \mid c(c_1) \cdot \bar{a}(b', c') \cdot c'(c_2) \cdot \mathbf{0}_*) \\ + c(c_1) \cdot \bar{a}(b', c') \cdot c'(c_2) \cdot \tau \cdot \boldsymbol{\nu} d'' (Q \mid R\{d'/d\}) \end{array} \right)$$

where $\mathbf{0}_*$ indicates an active process that cannot perform any action (e.g., $\boldsymbol{\nu}b_2(\bar{b}_2 \cdot \mathbf{0})$). (This equality holds under any visibility, hence we use the symbol $\cong$.)

If we replaced the second output at $a$ with an output at a different free name, say $a'$, then the processes could still be typable, and the equalities above would still hold. However, the equalities would not hold if we replaced the second output at $a$ with an output at $c_1$. Indeed, while the environment may not store $b$ or $c$ for using them in a later call at $a$ (or at an unrelated name such as $a'$), the environment is allowed to use $b$ and $c$ within services that are created following the first call at $a$; for instance, the environment could be

$$a(b, c) \cdot \bar{c}(c_1) \cdot !c_1(c'_1) \cdot \bar{b}(d'') \cdot \mathbf{0}$$

The following example illustrates the use of visibility to perform garbage-collection on names that will never be used. We refer to Appendix B.3 for the full definition of the corresponding pruning function.

**Example 14.** Consider a typing environment $\Delta$, a $\Delta$-process

$$P \stackrel{\text{def}}{=} !a. Q_1 \mid !b. \bar{c}. !a. Q_2 \mid !d. \bar{a}. \mathbf{0}$$

and a visibility $\Gamma$ compatible with $\Delta$ such that $\Gamma \cup \Delta$ is transitive. $\Gamma$ is intended here to represent the observer's visibility. Suppose $a \notin \Gamma(\*)$; that is, the observer is active but its current visibility does not include $a$ (which may however be in the visibility of other names in $\Gamma$). We then have $P \cong_{\Gamma}^{\Delta} !b. \bar{c}. \mathbf{0}$. The pruning is possible because, intuitively, the transitivity of $\Delta \cup \Gamma$ ensures us that an observer, whenever active, cannot have $a$ in its current visibility. For instance, if the observer interrogates $b$, then the transitivity of the visibility functions ensures us that $a \notin \Delta(b)$; then $c \in \Delta(b)$ (which is necessary for $P$ to be typable) gives us also $a \notin \Gamma(c)$. Similarly, exploiting transitivity, we deduce that also $d \notin \Gamma(\*)$, and that an observer may never be able to interrogate $d$; thus we can also remove the input on $d$.
<figure><img src="image_3.png" /><figcaption>Figure 2: Visible LTS</figcaption></figure>

# 4 Labelled Semantics

## 4.1 Trace-based proof techniques

The definition of may-testing makes use of contextual quantifications. We study here proof techniques without such quantifications, as forms of trace equivalence. For lack of space, analogous proof techniques for barbed equivalence are only reported in Appendix C. The first step is to express the transitions for a process that are allowed by an observer subject to certain visibility constraints. We call these the *type-allowed transitions*. They are of the form $[\Gamma] P \xrightarrow{\mu} [\Gamma'] P'$, to be read ‘an observer that has visibility $\Gamma$ allows process $P$ to make a transition $\mu$ and, as a result of the transition, the process becomes $P'$ and the visibility of the observer becomes $\Gamma'$. Type-allowed transitions are defined by the rules in Figure 2. Intuitively, an observer typable under $\Gamma$ can initially test inputs of processes at names in $\Gamma(*)$, if $\Gamma \downarrow *$, and outputs of processes in $\text{dom}(\Gamma)$ otherwise. The weak transitions $\Rightarrow$ and $\Rightarrow^\mu$ are defined in the usual manner from the strong one; for instance, $[\Gamma] P \Rightarrow^\mu [\Gamma'] P'$ holds if $[\Gamma] P \Rightarrow [\Gamma] P''$, and $[\Gamma] P'' \xrightarrow{\mu} [\Gamma'] P'''$, and $[\Gamma'] P''' \Rightarrow [\Gamma'] P'$, for some $P''$ and $P'''$.

An action $\tau$ is called a *reduction* (or an *internal action*); the remaining actions are called *interactions*. We use $\mathcal{T}$ to range over traces, which are finite sequences of interactions $\mu_1 \dots \mu_n$ ($n \ge 0$) in which the bound names are all distinct and different from the free names (the definition of bound and free names is as for processes, viewing a trace as a sequence of prefixes). A trace $\mu_1 \dots \mu_n$ is *trace of $P_0$ under visibility* $\Gamma_0$ if there are $P_i$, $\Gamma_i$ with $[\Gamma_i] P_i \stackrel{\mu_i}{\Rightarrow} [\Gamma_{i+1}] P_{i+1}$, for $0 \le i < n$.

**Definition 15** (Typed trace equivalence). Two $\Delta$-processes $P$ and $Q$ are *trace equivalent at* $\Gamma$, written $P \cong_{\Gamma} Q$, if $\Delta$, $\Gamma$ are compatible and $P$, $Q$ have the same sets of traces under $\Gamma$.

We show the main compositionality lemmas, and a trace-based characterisation of may testing. Other technical lemmas needed in proofs may be found in Appendix B.2.

**Lemma 16** (Restriction). If $P \cong_{\Delta} Q$ then also $\nu a P \cong_{\Delta^{-a}} \nu a Q$.

**Lemma 17** (Input). If $P \cong_{\Delta} Q$ and $\Gamma \nparallel *$; then also $a(x, b)$. $P \cong_{\Delta^{-*,b}} (\Gamma;* \to \Gamma(b))^{-b} a(x, b)$. $Q$.

**Lemma 18** (Output). If $P \cong_{\Delta} Q$ and $\Gamma \nparallel *$, then also $\bar{a}\langle e \rangle(b)$. $P \cong_{(\Delta;* \to \Delta(b))^{-b}} \bar{a}\langle e \rangle(b)$. $Q$.
**Lemma 19 (Parallel composition).** Suppose $P \leq_{\Delta}^{\Gamma} Q$ and $(\Gamma_1, \Gamma_2) \in \mathbf{split}(\Gamma)$. Then $\Gamma_2 \vdash R$ implies $P \mid R \leq_{(\Delta \cup \Gamma_2)^+}^{\Gamma_1} Q \mid R$ where $(-)^+$ indicates the transitive closure.

In the proof of Lemma 19, a trace of $P \mid R$ is split into a trace for $P$ and one for $R$. We have then to ensure that the condition of the lemma are maintained throughout the trace, notwithstanding modifications of the visibility functions. Some care is needed in case of synchronisations between $P$ and $R$, where the typing of the external observer has to remain the same; we also use the restriction Lemma 16. Other cases also exploit the extension Lemma 36, and the transitivity of the visibility function, to make sure that the views on free names are not increased along the trace.

**Theorem 20 (Characterisation of may testing using trace equivalence).** Suppose $\Delta \vdash P, Q$ then $P \leq_{\Delta}^{\Gamma} Q$ if and only if $P \cong_{\Delta}^{\Gamma} Q$.

The sketch of the proofs is the same as for characterisations of may testing with trace equivalence in untyped calculi, exploiting substitutivity properties of trace equivalence in the case of Soundness, and reason by contradiction in the case of Completeness. In addition, one has to take care of the observer visibilities, how it changes, and use type-allowed transitions. A similar results of characterisation also hold for barbed equivalence, using a typed form labelled bisimilarity, and are presented in Appendix C.

We can use typed trace equivalence to prove equalities such as those in Examples 13 and 14; the proofs are simple, following the definition of the equivalence and exploiting type-allowed transitions. See also Appendix B.3 for the proof about the pruning function that generalises Example 14. (Similarly, the proofs can be carried out for barbed equivalence, using the labelled bisimilarity in Appendix C.)

## 4.2 Visibility property on traces

We formalise the link between our type system and the notion of visibility in game semantics [6]. The reader not familiar with game semantics may safely skip the section. In game semantics, the notions of visibility and well-bracketing are defined based on a justification relation between moves performed by Player. These moves correspond to interactions on higher-order names in our setting, and the notion of justification can be formulated as follows.

**Definition 21.** Let $\mu_1, \mu_2$ be two interactions at HO names. We say that $\mu_1$ *justifies* $\mu_2$, noted $\mu_1 \prec \mu_2$, if: (i) either $\mu_1 = a\langle v \rangle(b)$ and $\mu_2 = \bar{b}\langle v' \rangle(c)$, or (ii) $\mu_1 = \bar{a}\langle v \rangle(b)$ and $\mu_2 = b\langle v' \rangle(c)$. When this is not the case, we write $\mu_1 \not\prec \mu_2$.

$\mu_1 \prec \mu_2$ captures the dependency induced by the fact that $\mu_2$ performs an interaction at a name that has been previously introduced by $\mu_1$. In contrast with the situation in game semantics, though, there is no notion of question and answer in our setting.

We can now define the notion of view. In the definition below, we allow a starting visibility $A$, because we want to consider processes that already have some knowledge about the observer (Opponent).
**Definition 22 (View).** Given $A \subseteq HO$, we define the view with starting visibility $A$ of a trace $T$, written $\text{view}_A(T)$, as follows:

$$ \text{view}_A(\varepsilon) = A \qquad \text{view}_A(\mathcal{T}_1\mu_1\mathcal{T}_2\mu_2) = \text{view}_A(\mathcal{T}_1) \cup \text{nHO}(\mu_1) \cup \text{nHO}(\mu_2) \text{ if } \mu_1 \prec \mu_2 \\ \text{view}_A(\mu_0 \dots \mu_n) = A \cup \text{nHO}(\mu_n) \text{ if } \forall 0 \le i \le n-1, \mu_i \nsim \mu_n $$

where $\text{nHO}(\mu)$ denotes the set of higher-order names appearing in the action $\mu$.

Views capture the idea that when an action is justified by another one, the names created in between must have been forgotten, otherwise this would mean that the process had the ability to store these names in order to reuse them. In the last clause in Definition 22, the action is justified by an action that happened before the beginning of the trace, therefore it has the starting visibility. In particular, $\text{view}_0(T)$ yields the usual definition in game semantics.

**Definition 23 (Respecting views).** Consider $A \subseteq HO$, a trace $(\mu_0 \dots \mu_n)$ respect views under starting visibility $A$ if $\text{fn}(\mu_0) \subseteq A$ and $\forall 1 \le i \le n, \text{fn}(\mu_i) \subseteq \text{view}_A(\mu_0 \dots \mu_{i-1})$

**Lemma 24.** Consider $\Delta, \Gamma, P$ such that $\Delta \vdash P, \Gamma$ is compatible with $\Delta$, and $\Delta \cup \Gamma$ is transitive. Let $A = (\Gamma \cup \Delta)(*)$, then every trace of $P$ under visibility $\Gamma$ respects views with starting visibility $A$.

The idea of the proof is that for a trace $(\mu_0 \dots \mu_n)$ there exist $P_0, \dots, P_{n+1}, \Delta_0, \dots, \Delta_n, \Gamma_0, \dots, \Gamma_{n+1}$ such that $P_0 = P, \Delta_0 = \Delta, \Gamma_0 = \Gamma$ and for all $0 \le i \le n, [\Gamma_i] P_i \xrightarrow{\mu_i} [\Gamma_{i+1}] P_{i+1}$ and $\Delta_i \vdash P_i$. We show by induction that for each $1 \le i \le n, (\Gamma_i \cup \Delta_i)(*) \subseteq \text{view}_A(\mu_0 \dots \mu_{i-1})$; it thus follows that the trace respects views under starting visibility $A$. The condition of $\Delta \cup \Gamma$ being transitive is crucial, otherwise $(\Gamma_i \cup \Delta_i)(*)$ could grow in unwanted ways.

# 5 Adding Well-Bracketing

## 5.1 Type system

In the previous sections we have studied visibility in connection with sequentiality. In this section we do the same for a refinement of sequentiality, namely well-bracketing. We begin by reviewing well-bracketing, following [3], and then outline how visibility is accommodated.

**From sequentiality to well-bracketing.** In languages without control operators, well-bracketing intuitively means that return-call interactions among terms follow a stack-based discipline. In a well-bracketed system, a service that is interrogated, say $S$, acquires the thread and is supposed to return a final result (unless the computation diverges) thus releasing the thread. During its computation, $S$ may however interrogate another service, say $T$, which, upon completion of its computation, will return the result to $S$; service $S$ must receive the answer from $T$ before returning the final result. The implementation of this policy requires continuation names, that are used to handle the return messages. When a service is
interrogated, it receives a fresh continuation name that is used once, in output, to deliver the final result. Accordingly, a client that has interrogated the service will use the continuation name in input to receive the result. Thus continuation names are *linear* [10] — they may only be used once. In contrast with [3], we do not require *receptiveness* [22] — the input-end of the name needs not be made available as soon as the name is created. Enforcing only linearity allows us to gain flexibility. To ensure the well-bracketing policy, the type system in [19] makes use of stacks.

**Definition 25 ([19]).** A stack, $\sigma$, is a sequence of input- and output- tagged continuation names, in which the input and output tags alternate:

$$ \sigma ::= \sigma_0 | \sigma_I $$

$$ \sigma_0 ::= p^0, \sigma_I | \emptyset $$

$$ \sigma_I ::= p^I, \sigma_0 | \emptyset $$

Moreover: a name may appear at most once with a given tag; and, if a name appears with both tags, then the input occurrence should immediately follow the output occurrence.

We write $p^0 \in \sigma$ (resp. $p^I \in \sigma$) if there is an occurrence of $p^0$ (resp. $p^I$) in $\sigma$. We write $p \in \sigma$ if either $p^0 \in \sigma$ or $p^I \in \sigma$.

Intuitively, a stack expresses the expected usage of the free continuation names in a process. For instance, if $P$ can be typed using stack $p_1 : o, p_2 : i, p_3 : o, p_3 : i, p_4 : o$, then $p_1, \dots, p_4$ are the free continuation names in $P$; among these, $p_1$ will be used first, in an output; then $p_2$ will be used, in an input interaction with the environment. $P$ possesses both the output and the input capability on $p_3$, so it shall perform a reduction at $p_3$; the computation for $P$ terminates with an output at $p_4$. This behaviour however concerns only the free continuation names of $P$: at any time when an output usage is expected, $P$ may decide to create a new continuation name and send it out, maintaining its input end.

**Visibility.** We now discuss how to combine the visibility in Section 3 with well-bracketing. Higher-order names are partitioned into the set SER of server names, and the set CON of continuation names. Now $a, b, c$ range over server names, while $p, q, r$ range over continuation names. By convention, server names carry a triple consisting of a first-order value, a server name and a continuation; whereas continuations carry a first-order value and a server name. Accordingly, outputs on higher-order names are of the form $\bar{a}\langle n \rangle(b, p)$ and $\bar{p}\langle n \rangle(b)$, and similarly for inputs. First-order names are as before.

Visibility functions are then transitive partial functions from SER $\cup$ CON $\cup$ $\{*\}$ to $P_{fin}(SER \cup CON)$. Server names are handled essentially like HO names in Section 3. In contrast, some care is needed on continuation names because they are linear. For this reason, some of the notations for handling visibility functions have to be revisited. A visibility function $\Delta$ is *duplicable*, written $\Delta \dot{=} \Delta$, if $\mathrm{dom}(\Delta) \subseteq \mathrm{SER}$. This predicate is useful to insure that continuation names are used linearly. In particular, the definition of splitting is refined as follows: $\mathrm{split}(\Delta)$ is the set of pairs $(\Delta_1, \Delta_2)$ such that $\Delta_1 \cup \Delta_2 = \Delta$ and $(\Delta_1 \cap \Delta_2) \dot{=} \Delta$.

Typing environments include a stack; thus a typing environment is a pair $\langle \Delta | \sigma \rangle$ of a visibility function and a stack. In the typing rule for parallel composition, we rely on splitting as well as on $\mathrm{inter}(\sigma_1, \sigma_2)$, the interleaving of stacks $\sigma_1$ and $\sigma_2$.
<figure><img src="image_4.png" /><figcaption>Figure 3: Typing rules with visibility and stack</figcaption></figure>

**Definition 26 (Interleaving).** We write $\sigma_1 \in \mathbf{inter}(\sigma_2; \sigma_3)$ if (i) $\sigma_1$ is a stack, and (ii) $\sigma$ is an interleaving of $\sigma_2$ and $\sigma_3$ as by the following inductive rules:

1. $\emptyset \in \mathbf{inter}(\emptyset; \emptyset)$

2. $p:0, \sigma_1 \in \mathbf{inter}(\sigma_2; p:0, \sigma_3)$ if $\sigma_1 \in \mathbf{inter}(\sigma_2; \sigma_3)$

3. $p:0, \sigma_1 \in \mathbf{inter}(p:0, \sigma_2; \sigma_3)$ if $\sigma_1 \in \mathbf{inter}(\sigma_2; \sigma_3)$

4. the same as (2) and (3) with $p: i$ instead of $p: o$

If a name appears both in $\sigma_2$ and in $\sigma_3$ with the same tag, then $\mathbf{inter}(\sigma_2; \sigma_3)$ is empty. Figure 3 gives the typing rules. The rules combine the handling of visibility and the update of the stack. For instance, in rule **O-SER**, newly created names $b$ and $p$ are added to the visibility when typing the continuation $P$, and $p^I$ is added on top of the stack, meaning that $P$ shall perform an input at $p$ before interacting on other continuation names. The output capability on $p$ is transmitted along the output at $a$; correspondingly, in rules **I-SER<sub>1</sub>** and **I-SER<sub>2</sub>**, $p^0$ is added to $\sigma$. In contrast with [3], we do not impose $\sigma = \emptyset$ in rule **I-SER<sub>1</sub>**, as we do not enforce input receptiveness on continuation names. Performing inputs and outputs at continuation names has the effect of consuming the corresponding particle on top of the stack. The stack is empty when typing a replicated input, so to avoid duplication of continuation names. In rules **I-SER<sub>2</sub>** and **NIL**, we need to check that $\Delta$ is duplicable to make sure that all the input on continuations are defined. Rules **SUCC**, **O-FO**, **I-FO**, **RES-FO**, **SUM** and **IF** are like in Figure 1, and are omitted.

**Theorem 27 (Subject reduction).** Suppose $\langle \Delta | \sigma \rangle \vdash P$ and $P \xrightarrow{\mu} P'$. We have:
* if $\mu = \tau$, then either $\sigma = p^0, p^I, \sigma''$ with $p \in \mathbf{Ncon} \setminus \mathbf{fn}(P')$, in which case $\langle \Delta^{-p} | \sigma'' \rangle \vdash P'$,
or $\langle \Delta | \sigma \rangle \vdash P'$;

* if $\mu = \bar{a}\langle v \rangle(b, p)$ then $a \in \Delta(*)$ and $\langle \Delta^{-*}; b \mapsto \Delta(*), b; p \mapsto \Delta(*), b | p^I, \sigma \rangle \vdash P'$;

* if $\mu = \bar{p}\langle v \rangle(b)$ then $\sigma = p^0, \sigma''$, $p \in \Delta(*)$ and $\langle \Delta^{-*}; b \mapsto \Delta(*), b | \sigma'' \rangle \vdash P'$;

* if $\mu = a\langle v \rangle(b, p)$ and $\Delta \nparallel *$ then $\langle \Delta; * \mapsto \Delta(a), b, p | p^0, \sigma \rangle \vdash P'$;

* if $\mu = p\langle v \rangle(b)$ and $\Delta \nparallel *$ then $\sigma = p^I, q^0, \sigma''$ and $\langle \Delta^{-p}; * \mapsto \Delta(p), b | q^0, \sigma'' \rangle \vdash P'$;

* if $\mu = h\langle v \rangle$ or $(\mu = \bar{h}\langle v \rangle$ and $\Delta \nparallel *)$ then $\langle \Delta | \sigma \rangle \vdash P'$.

As previously, we have to define compatibility of typing environments so to be able to use the contextual forms of behavioural equivalence from Section 2.

**Definition 28.** $\langle \Delta_1 | \sigma_1 \rangle$ and $\langle \Delta_2 | \sigma_2 \rangle$ are compatible if $(\Delta_1 \cap \Delta_2) \ni$ and $\mathbf{inter}(\sigma_1, \sigma_2) \neq \emptyset$.

**Example 29.** Consider the process

$$ P \stackrel{\text{def}}{=} \nu h ( \overline{h} \langle 5 \rangle | \\ \overline{a}(b, q). ( !b(p). h(x). (\overline{h} \langle x + 1 \rangle. \mathbf{0} | \overline{p}. \mathbf{0}) | \\ q. h(x). \overline{h} \langle x \rangle. \overline{c}(d, r). r. h(y). \overline{h} \langle y \rangle. \text{ if } x = y \text{ then } \overline{s}. \mathbf{0} \text{ else } \mathbf{0}_* ) $$

Here $h$ is used as an integer reference, initially set to 5. The process calls a service $a$, giving access to a name $b$ that can be used to increment the reference. When the call at $a$ returns (at $q$), the reference is read twice and, in between, a call at $c$ is made. Without visibility, the two values read for $h$ might be different: as $b$ has been exported, the environment could freely use $b$ and increment the reference in between the two reads. Visibility ensures us that, when the initial call at $a$ is returned, name $b$ is ‘forgotten’ by the environment, which cannot therefore use it anymore. Thus, if $Q$ is the process defined like $P$ but with the last line replaced with $q. \overline{c}(d, r). r. \overline{s}. \mathbf{0}$, then we have $P \cong Q$. We refer to Appendix D.1 for an ML-like presentation of the example above, as well as for a longer example, also showing how re-entrant calls may sometimes make visibility boundaries hard to predict.

## 5.2 Labelled semantics

To represent the point of view of the observer, we use typing environments of the form $[\Gamma | \kappa]$, where $\Gamma$ is a visibility function and $\kappa$ is a stack. Figure 4 defines the typed transitions, written $[\Gamma | \kappa] P \xrightarrow{\mu} [\Gamma' | \kappa'] P'$. Rules TrTau, Tr0-fo and TrI-fo are similar to their counterpart in Figure 2, and are omitted.

A trace $\mu_1 \dots \mu_n$ is a *well-bracketed trace of $P_0$ under* $[\Gamma_0 | \kappa_0]$ if there are $P_i, \Gamma_i, \kappa_i$ ($1 \le i \le n$) with $[\Gamma_i | \kappa_i] P_i \stackrel{\mu_i}{\implies} [\Gamma_{i+1} | \kappa_{i+1}] P_{i+1}$ for all $0 \le i < n$.
$$
\begin{align*}
\text{TrO-ser} &\xrightarrow{P \xrightarrow{\bar{a}\langle v \rangle(b,p)} P'} a \in \text{dom}(\Gamma) \quad \Gamma \nmid_* \\
&\xrightarrow{[\Gamma \mid \kappa] P \xrightarrow{\bar{a}\langle v \rangle(b,p)} [\Gamma; * \mapsto \Gamma(a), b, p \mid p^0, \kappa] P'} \\[1.5em]
\text{TrO-con} &\xrightarrow{P \xrightarrow{\bar{p}\langle v \rangle(b)} P'} p \in \text{dom}(\Gamma) \quad \Gamma \nmid_* \\
&\xrightarrow{[\Gamma \mid p^1, q^0, \kappa] P \xrightarrow{\bar{p}\langle v \rangle(b)} [\Gamma^{-p}; * \mapsto \Gamma(p), b \mid q^0, \kappa] P'} \\[1.5em]
\text{TrI-ser} &\xrightarrow{P \xrightarrow{a\langle v \rangle(b,p)} P'} a \in \Gamma(*) \\
&\xrightarrow{[\Gamma \mid \kappa] P \xrightarrow{a\langle v \rangle(b,p)} [\Gamma^{-*}; p \mapsto \Gamma(*), b; b \mapsto \Gamma(*), b \mid p^1, \kappa] P'} \\[1.5em]
\text{TrI-con} &\xrightarrow{P \xrightarrow{p\langle v \rangle(b)} P'} p \in \Gamma(*) \\
&\xrightarrow{[\Gamma \mid p^0, \kappa] P \xrightarrow{p\langle v \rangle(b)} [\Gamma^{-*}; b \mapsto \Gamma(*), b \mid \kappa] P'}
\end{align*}
$$

<caption>Figure 4: Visible LTS with stack</caption>

**Definition 30** (Typed trace equivalence). Two $\langle\Delta | \sigma\rangle$-processes $P$ and $Q$ are trace equivalent at $[\Gamma | \kappa]$, written $P \stackrel{[\Gamma|\kappa]}{\cong} Q$, if $\langle\Delta | \sigma\rangle$ and $[\Gamma | \kappa]$ are compatible and $P$ and $Q$ have the same sets of well-bracketed traces under $[\Gamma | \kappa]$.

This typed version of trace equivalence enjoys properties, including substitutivity properties, similar to those of the trace equivalence in Section 4. We only report the characterisation result with respect to may testing.

**Theorem 31** (Characterisation of may testing using trace equivalence). Suppose $\langle\Delta | \sigma\rangle \vdash P, Q$; then $P \stackrel{[\Gamma|\kappa]}{\cong} Q$ if and only if $P \stackrel{[\Delta|\sigma]}{\cong} Q$.

The analogous result for typed bisimilarity is in Appendix D, together with results about the shape of type-allowed traces akin to those in Section 4.2.

# 6 Conclusions and Future Work

In this paper we have studied the meaning of visibility, originating from game-semantics interpretations of typed $\lambda$-calculi and reflecting absence of higher-order store, in a calculus of pure name-passing such as the $\pi$-calculus. In contrast with $\lambda$-calculi, in the $\pi$-calculus there is no explicit notion of store, and no unique identities (e.g., the input end of a name may have multiple occurrences, arbitrarily structured). These aspects determine considerable differences in the semantic analysis of visibility. For instance, in the $\pi$-calculus visibility has to be enforced by means of a dedicated type system; and the visibility functions have to satisfy special properties such as transitivity. We have highlighted such differences, and investigated the behavioural effects of visibility. In particular, we have shown full abstract
characterisations of may testing and barbed equivalence, as form of trace equivalence and labelled bisimilarity.

There are several directions for future work that we would like to pursue. In game semantics, further aspects related to first-order store have been studied; for instance allowing first-order references as values (that can be passed around) [12, 8], or allowing to store first-order references (i.e., references with types such as `int ref ref [16, 9]`). We would like to investigate the effects of such distinctions on our types and proof techniques.

We have worked with $\pi$I, a dialect of $\pi$-calculus in which all names exchanged are newly created. Thus $\pi$I lacks the free-output construct, where the communication of existing names is permitted. As shown in the literature [4, 24, 7], $\pi$I is closer to game semantics than the standard $\pi$-calculus. We would like to see whether our results can be adapted so to accommodate also the free output construct. While free output can be modelled in $\pi$I [2], it allows a direct representation of idioms such as ‘delegate to someone else the task of answering’, or the expression of tail-call recursion.

We have studied visibility on top of type systems for sequentiality and well-bracketing. Allowing concurrency would probably require relaxing the definition of the visibility functions; we leave the details to future work.

## References

[1] Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming languages. *Found. Trends Program. Lang.*, 3(2-3):95-230, 2016. doi:10.1561/2500000031.

[2] Michele Boreale. On the expressiveness of internal mobility in name-passing calculi. *Theor. Comput. Sci.*, 195(2):205-226, 1998. doi:10.1016/S0304-3975(97)00220-X.

[3] Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On sequentiality and well-bracketing in the $\pi$-calculus. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE, June 2021. URL: http://dx.doi.org/10.1109/LICS52264.2021.9470559, doi:10.1109/lics52264.2021.9470559.

[4] Kohei Honda. Processes and games. In Fabio Gadducci and Ugo Montanari, editors, *Fourth International Workshop on Rewriting logic and Its Applications, WRLA2002, Pisa, Italy, 19-21, 2002*, volume 71 of *Electronic Notes in Theoretical Computer Science*, pages 40-69. Elsevier, 2002. doi:10.1016/S1571-0661(05)82528-9.

[5] Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Han-kin, editor, *Programming Languages and Systems - ESOP'98, 7th European Symposium*
on Programming, 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, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567, doi:10.1007/BFB0053567.

[6] Guilhem Jaber and Andrzej S. Murawski. Complete trace models of state and control. In Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, page 348-374, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-72019-3_13.

[7] Guilhem Jaber and Davide Sangiorgi. Games, Mobile Processes, and functions. In CSL 2022 - 30th EACSL Annual Conference on Computer Science Logic, pages 1-35, Göttingen, Germany, February 2022. URL: https://hal.science/hal-03407123.

[8] Guilhem Jaber and Nikos Tzevelekos. Trace semantics for polymorphic references. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 585-594. ACM, 2016. doi:10.1145/2933575.2934509.

[9] Ohad Kammar, Paul B. Levy, Sean K. Moss, and Sam Staton. A monad for full ground reference cells. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 2017. IEEE. doi:10.1109/LICS.2017.8005109.

[10] Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst., 21(5):914-947, 1999. doi:10.1145/330249.330251.

[11] Naoki Kobayashi and Davide Sangiorgi. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst., 32(5):16:1-16:49, 2010. doi:10.1145/1745312.1745313.

[12] James Laird. A fully abstract trace semantics for general references. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings, volume 4596 of Lecture Notes in Computer Science, pages 667-679. Springer, 2007. doi:10.1007/978-3-540-73420-8_58.

[13] R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, LFCS, 1991. Also in Logic and Algebra of Specification, ed. F.L. Bauer, W. Brauer and H. Schwichtenberg, Springer Verlag, 1993.

[14] Robin Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119-141, June 1992. doi:10.1017/S0960129500001407.
[15] Robin Milner. Functions as processes. *Math. Struct. Comput. Sci.*, 2(2):119-141, 1992.
doi:10.1017/S0960129500001407.

[16] Andrzej S. Murawski and Nikos Tzevelekos. Algorithmic games for full ground references. *Formal Methods in System Design*, 52(3):277-314, 2018.
doi:10.1007/s10703-017-0292-9.

[17] Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Thomas A. Henzinger and Dale Miller, editors, *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 72:1-72:10. ACM, 2014. doi:10.1145/2603088.2603116.

[18] Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. *Math. Struct. Comput. Sci.*, 6(5):409-453, 1996. URL: https://doi.org/10.1017/s096012950007002x, doi:10.1017/S096012950007002X.

[19] Enguerrand Prebet. *Typed Behavioural Equivalences in the Pi-Calculus*. Theses, Ecole normale supérieure deyon - ENS LYON ; Université degli studi (Bologne, Italie), September 2022. URL: https://hal.science/tel-03920089.

[20] Davide Sangiorgi. The lazy lambda calculus in a concurrency scenario. *Inf. Comput.*, 111(1):120-153, 1994. URL: https://doi.org/10.1006/inco.1994.1042, doi:10.1006/INCO.1994.1042.

[21] Davide Sangiorgi. pi-calculus, internal mobility, and agent-passing calculi. *Theor. Comput. Sci.*, 167(1&2):235-274, 1996. doi:10.1016/0304-3975(96)00075-8.

[22] Davide Sangiorgi. The name discipline of uniform receptiveness. *Theor. Comput. Sci.*, 221(1-2):457-493, 1999. doi:10.1016/S0304-3975(99)00040-7.

[23] Nobuko Yoshida, Martin Berger, and Kohei Honda. Strong normalization in the pi-calculus. *Inf. Comput.*, 191(2):145-202, 2004. URL: https://doi.org/10.1016/j.ic.2003.08.004, doi:10.1016/J.IC.2003.08.004.

[24] Nobuko Yoshida, Simon Castellan, and Léo Stefanesco. Game semantics: Easy as pi. *CoRR*, abs/2011.05248, 2020. URL: https://arxiv.org/abs/2011.05248, arXiv:2011.05248.

A Section 2: Definition of the Operational Semantics

*Structural congruence*, written ≡, is the smallest relation that is an equivalence relation, contains α-conversion, is preserved by all operators of the calculus, and satisfies the following
axioms:

$$ \overline{P \mid Q \equiv Q \mid P} $$

$$ \overline{P \mid (Q \mid R) \equiv (P \mid Q) \mid R} $$

$$ \overline{P \mid 0 \equiv P} $$

$$ \overline{P + Q \equiv Q + P} $$

$$ \overline{P + (Q + R) \equiv (P + Q) + R} $$

$$ \overline{P + 0 \equiv P} $$

$$ \overline{a \notin \mathit{fn}(Q) \qquad (\nu a P) \mid Q \equiv \nu a(P \mid Q)} $$

$$ \overline{\nu a \nu b P \equiv \nu b \nu a P} $$

$$ \overline{!\alpha. P \equiv !\alpha. P \mid \alpha. P} $$

Similar versions of axioms for restrictions of the form $\nu h$ instead of $\nu a$ have been omitted.

To define the labelled transition system (LTS), we introduce actions, defined by the following grammar:

$$ \mu ::= \tau \mid a\langle v \rangle(b) \mid \bar{a}\langle v \rangle(b) \mid h\langle v \rangle \mid \bar{h}\langle v \rangle \mid \omega $$

Actions are early for first-order values, and late for the transmission of HO names. We write $bn(\mu)$ (resp. $fn(\mu)$) for the bound (resp. free) names of action $\mu$, defined by saying that $b$ is a bound name in actions $a\langle v \rangle(b)$ and $\bar{a}\langle v \rangle(b)$, and the other names in actions are free.

We suppose that any closed first-order expression $e$ can be evaluated to some value $v$. We write $e \downarrow v$ for the corresponding evaluation relation. We furthermore suppose that equality between values can be tested.

The LTS is defined, on closed processes, by the rules in Figure 5.

We write $P \downarrow_\omega$ if $P \xrightarrow{\omega} \omega$, i.e., if $P$ contains an unguarded occurrence of an $\omega$ prefix at toplevel. We write $P \nrightarrow_\omega$ when this is not the case.

# B Additional Material for Section 3

## B.1 Properties of the type system

**Lemma 32.** Suppose $\Delta \vdash P$ and $a \notin fn(P)$. Then also $\Delta^{-a} \vdash P$.

**Lemma 33** (Invariance of typing w.r.t. structural congruence). If $\langle\Delta|\sigma\rangle \vdash P$ and $P \equiv P'$, then also $\langle\Delta|\sigma\rangle \vdash P'$.

## B.2 Properties of trace equivalence

**Lemma 34** (Shrinking). Suppose $\Gamma' \subseteq \Gamma$, $\Delta$ and $\Gamma'$ compatible and $P \cong_{\Delta}^{\Gamma} Q$. Then also $P \cong_{\Gamma'}^{\Delta} Q$.

**Definition 35** (Projection). Let $\Gamma$ be a visibility function and $N$ a set of names. We define a visibility function as follows:

$$ \mathbf{proj}(N, \Gamma) : \begin{array}{rcl} \mathbf{HO} \cup \{ * \} & \to & \mathcal{P}(\mathbf{HO}) \\ a \in \mathrm{dom}(\Gamma) \cap N & \mapsto & \Gamma(a) \cap N \end{array} $$
<figure><img src="image_5.png" /><figcaption>Figure 5: Labelled transition semantics.
Symmetric versions of the rules for parallel composition and for sum have been omitted.</figcaption></figure>

**Lemma 36 (Extension).** Consider $\Delta, \Gamma, \Gamma', P, Q$ such that $\text{proj}(\text{fn}(\Gamma, P, Q), \Gamma') = \Gamma$ and $\Delta$ and $\Gamma'$ are compatible. If $P \stackrel{\Delta}{\le} \Gamma$ $Q$ then $P \stackrel{\Delta}{\le} \Gamma'$ $Q$.

In the statement above, $\text{fn}(\Gamma, P, Q)$ stands for the union of all names mentioned in $\Gamma$, together with the names occurring free in $P$ and $Q$.

## B.3 Pruning Processes using Types

Consider a visibility function $\Delta$ and $S \subseteq \mathbf{HO}$. We write $\alpha \frown S$ when $\alpha$ is an input of the form $a(x, b)$ and either $a \in S$ or $(a \in \text{dom}(\Delta)) \text{ and } \Delta(a) \cap S \neq \emptyset$).

We define inductively the pruning function on processes that removes all instances of the names in $S$ as follows:

$$ \mathrm{Pr}_S^\Delta(\alpha. P) = \begin{cases} \mathbf{0} & \text{if } \alpha \frown S \\ \alpha. \mathrm{Pr}_S^\Delta(P) & \text{otherwise} \end{cases} \qquad \mathrm{Pr}_S^\Delta(!\alpha. P) = \begin{cases} \mathbf{0} & \text{if } \alpha \frown S \\ !\alpha. \mathrm{Pr}_S^\Delta(P) & \text{otherwise} \end{cases} $$

$$ \mathrm{Pr}_S^\Delta(\bar{\alpha}. P) = \bar{\alpha}. \mathrm{Pr}_S^\Delta(P) \qquad \mathrm{Pr}_S^\Delta(\nu a. P) = \nu a. \mathrm{Pr}_S^\Delta(P) \qquad \mathrm{Pr}_S^\Delta(\nu h. P) = \nu h. \mathrm{Pr}_S^\Delta(P) $$

$$ \mathrm{Pr}_S^\Delta(P | Q) = \mathrm{Pr}_S^\Delta(P) | \mathrm{Pr}_S^\Delta(Q) \qquad \mathrm{Pr}_S^\Delta(P + Q) = \mathrm{Pr}_S^\Delta(P) + \mathrm{Pr}_S^\Delta(Q) \qquad \mathrm{Pr}_S^\Delta(\mathbf{0}) = \mathbf{0} $$

$$ \mathrm{Pr}_S^\Delta(\omega) = \omega \qquad \mathrm{Pr}_S^\Delta(\text{if } e = f \text{ then } P \text{ else } Q) = \text{if } e = f \text{ then } \mathrm{Pr}_S^\Delta(P) \text{ else } \mathrm{Pr}_S^\Delta(Q) $$
**Lemma 37 (Pruning).** Let $\Gamma, \Delta, P$ such $\Delta \vdash P$ and $\Gamma$ and $\Delta$ are compatible and $\Delta \cup \Gamma$ is transitive. Then for all $S \subseteq \mathbf{HO}$ such that $S \cap (\Gamma \cup \Delta(\ast)) = \emptyset$, $\Delta^{-S} \vdash \mathrm{Pr}_S^\Delta(P)$ and $P \cong_\Gamma^\Delta \mathrm{Pr}_S^\Delta(P)$.

We actually remove more than the names in $S$. Indeed, to preserve sequentiality, we
cannot simply remove an output; we actually remove all inputs that may cause an output
on the names in $S$.

The idea of the proof is to show that $S \cap (\Gamma \cup \Delta(\ast)) = \emptyset$ is an invariant throughout the trace; for this we use repeatedly transitivity of $\Gamma \cup \Delta$.

*Proof.* Let $\mu_1 \dots \mu_n$ a trace of $P$ under $\Gamma$, let $P_i, \Gamma_i$ be the processes and visibility functions given that trace and $\Delta_i$ the visibility functions given by subject reduction. We show by induction on $i$ that there exists $\Gamma'_i, \Delta'_i$ such that $\Gamma'_i \supseteq \Gamma_i$ and $\Delta'_i \supseteq \Delta_i$ and $S \cap (\Gamma'_i \cup \Delta'_i)(\ast) = \emptyset$ and that $\Delta'_i$ and $\Gamma'_i$ are compatible, have a transitive union and coincide on the intersection of their domains. The case $i=0$ is immediate, let $0 \le i < n$, we assume the induction hypothesis on $i$ and show it for $i+1$ by cases on $\mu_i$:

* if $\mu_i = \tau$, or $\mu_i = h\langle v \rangle$ or $\mu_i = \bar{h}\langle v \rangle$ then $\Gamma_{i+1} = \Gamma_i$ and $\Delta_{i+1} = \Delta_i$, these cases are immediate by setting $\Gamma'_{i+1} = \Gamma'_i$ and $\Delta'_{i+1} = \Delta'_i$.

* if $\mu_i = \bar{a}\langle v \rangle(b)$ then $\Gamma_{i+1} = \Gamma_i; \ast \mapsto \Gamma_i(a), b$ and $\Delta_{i+1} = \Delta_i^{-*}; b \mapsto \Delta_i(\ast), b$. Let $\Gamma'_{i+1} = \Gamma'_i; \ast \mapsto \Delta'_i(\ast), b \supseteq \Gamma_{i+1}$ because $a \in \Delta_i(\ast)$ therefore $\Gamma_i(a) \subseteq \Delta_i(\ast)$. And let $\Delta'_{i+1} = \Delta_i^{*-\ast}; b \mapsto \Delta'_i(\ast), b$.

$\Gamma'_{i+1}$ and $\Delta'_{i+1}$ are compatible, their union is transitive and they coincide on the inter-section of their domains.

$(\Gamma'_{i+1} \cup \Delta'_{i+1})(\ast) = (\Gamma'_i \cup \Delta'_i)(\ast), b$ where $b$ is fresh therefore $b \notin S$ and by induction hypothesis $S \cap (\Gamma'_{i+1} \cup \Delta'_{i+1})(\ast) = \emptyset$.

* if $\mu_i = a\langle v \rangle(b)$ the case is similar to the previous one, swapping $\Gamma$ and $\Delta$.

This ensures us that none of the $\mu_i$ are inputs or outputs on higher-order names in $S$. Moreover if $a \in \mathrm{dom}(\Delta)$ and $\Delta(a) \cap S \neq \emptyset$ then for all $i$, $a \notin (\Gamma_i \cup \Delta_i)(\ast)$ otherwise we would have $\emptyset \neq \Delta(a) \cap S = \Delta_i(a) \cap S \subseteq (\Gamma_i \cup \Delta_i)(\ast) \cap S = \emptyset$.

Therefore the trace $\mu_1 \dots \mu_n$ is also a trace of $\mathrm{Pr}_S^\Delta(P)$ under $\Gamma$. $\square$

# C Section 4: Labelled Bisimilarity

A *typed relation* is a set of triples $(\Gamma, P, Q)$ intended to represent the visibility of the observer for processes $P$ and $Q$ in the bisimulation game.

**Definition 38 (Typed Bisimulation).** A typed relation $\mathcal{R}$ is a *typed (weak) bisimulation* if whenever $(\Gamma, P, Q) \in \mathcal{R}$:

1. if $[\Gamma] P \xrightarrow{\mu} [\Gamma'] P'$ then there is $Q'$ such that $\Gamma Q \stackrel{\hat{\mu}}{\Rightarrow} \Gamma' Q'$ and $(\Gamma', P', Q') \in \mathcal{R}$;
2. the converse, on the actions from $Q$.

Typed bisimilarity, written $\approx$, is the largest typed bisimulation. For two $\Delta$-processes $P, Q$ we write $P \approx_{\Delta}^{\Gamma} Q$ when $(\Gamma, P, Q) \in \approx$ and $\Delta$ and $\Gamma$ are compatible. In this case, we say that $P$ and $Q$ are *bisimilar under* $\Gamma$.

**Example 39.** As for barbed equivalence the visibility of opponent also plays an important role in determining whether two process are bisimilar under some $\Gamma$. Consider $\Delta$ and $\Gamma$ compatible, and a $\Delta$-process of the form $Q = P | a. \bar{b}. R$ with $b \notin \mathbf{fn}(P)$ and $b \in \mathbf{dom}(\Gamma)$:

* if $a \in \mathbf{fn}(P)$, we may have, for example, $P = \bar{a}. R'$, in which case $Q \xrightarrow{\tau} R' | \bar{b}. R$; such derivative is not bisimilar with $P$ under $\Gamma$, as only $R' | \bar{b}. R$ can make an output on $b$;

* if $a \in \Gamma(*)$, then we have $Q \xrightarrow{a} P | \bar{b}. R$, which is not bisimilar to any $P'$ such that $P \xrightarrow{a} P'$, for the same reason as in the previous case;

* however, if both $a \notin \mathbf{fn}(P)$ and $a \notin \Gamma(*)$, then $Q$ cannot make an input on $a$, and therefore we have $Q \approx_{\Delta}^{\Gamma} P$.

The analogues of Lemmas 16-19 and 37 also hold for typed bisimilarity.

**Lemma 40 (Restriction).** If $P \approx_{\Delta}^{\Gamma} Q$, then also $\nu a P \approx_{\Delta-a}^{\Gamma-a} \nu a Q$.

**Lemma 41 (Input).** If $P \approx_{\Delta}^{\Gamma} Q$ and $\Gamma \nmid *$, then also $a(x, b)$. $P \approx_{\Delta-*, b}^{(\Gamma;* \to \Gamma(b))^{-b}} a(x, b)$. $Q$.

**Lemma 42 (Output).** If $P \approx_{\Delta}^{\Gamma} Q$ and $\Gamma \nmid *$, then also $\bar{a}\langle e \rangle(b)$. $P \approx_{(\Delta;* \to \Delta(b))^{-b}}^{\Gamma-*, b} \bar{a}\langle e \rangle(b)$. $Q$.

**Lemma 43 (Parallel composition).** Suppose $P \approx_{\Delta}^{\Gamma} Q$ and $(\Gamma_1, \Gamma_2) \in \text{split}(\Gamma)$. Then $\Gamma_2 \vdash R$ implies $P | R \approx_{(\Delta \cup \Gamma_2)+}^{\Gamma_1} Q | R$.

**Lemma 44 (Pruning).** Let $\Gamma, \Delta, P$ such $\Delta \vdash P$ and $\Gamma$ and $\Delta$ are compatible. Then for all $S \subseteq \mathbf{HO}$ such that $S \cap (\Gamma \cup \Delta(*) = \emptyset$, $\Delta^{-S} \vdash \text{Pr}_S^{\Delta}(P)$ and $P \approx_{\Delta}^{\Gamma} \text{Pr}_S^{\Delta}(P)$.

Technical lemmas similar to those for trace equivalence also holds, such as the following ones.

**Lemma 45 (Shrinking).** Suppose $\Gamma' \subseteq \Gamma$, $\Delta$ and $\Gamma'$ compatible and $P \approx_{\Delta}^{\Gamma} Q$. Then also $P \approx_{\Delta'}^{\Gamma'} Q$.

**Lemma 46 (extension).** Consider $\Gamma, \Gamma', P, Q$ such that $\text{proj}(\mathbf{fn}(\Gamma, P, Q), \Gamma') = \Gamma$ and $\Delta$ and $\Gamma'$ are compatible. If $P \approx_{\Delta}^{\Gamma} Q$ then $P \approx_{\Delta'}^{\Gamma'} Q$.

We report the characterisation results. Soundness follows from the substitutivity properties of labelled bisimilarity. For completeness, as usual with characterisations of barbed equivalence, the proof uses induction, via an inductive stratification of bisimilarity, and requires image-finiteness of processes (that is, up-to $\alpha$-conversion, the set of possible type-allowed weak transitions emanating from a process is finite). The image-finite condition is needed in the characterisation of bisimilarity via the inductive stratification. Also, and again in line with proofs about barbed relations, the proof exploits the presence of the sum operator and of success signals that can be emitted by a testing context whenever needed.
**Theorem 47** (Soundness of bisimilarity for barbed equivalence). Suppose $\Delta \vdash P, Q$ with $P \cong_{\Delta}^{\Gamma} Q$. Then also $P \cong_{\Delta}^{\Gamma} Q$.

**Theorem 48** (Completeness of bisimilarity for barbed equivalence). If $P$ and $Q$ are image-finite processes, and if $P \cong_{\Delta}^{\Gamma} Q$, then $P \cong_{\Delta}^{\Gamma} Q$.

# D Additional Material for Section 5

## D.1 About Example 29

The process discussed in Example 29 can be seen as the $\pi$-calculus counterpart of the following ML program, which might be more readable for a reader familiar with functional languages:

```
let h = ref 0 in
let b () = h := !h +1 in
begin
  a b;
  let x = !h in
  c x;
  let y = !h in
  if x=y then loop() else ()
end
```

**Re-entrant call.** The following example first shows an equality similar to that of Example 29; and then develops the example so to show how re-entrant calls may sometimes break 'expected' visibility boundaries.

We define two processes $P_1$ and $P_2$, which access a reference $h$ (implemented using a first-order name), and can call a server $b$. When calling $b$, the processes first pass the name incr of a server that increments the value stored in $h$. Once the call on $b$ is answered the processes read the value in $h$ and make another call to $b$ passing the identity function. After that, the processes read again the value of $h$. Finally, $P_1$ outputs the first value read in $h$ while $P_2$ outputs the second one.

$$ P_i \stackrel{\text{def}}{=} \bar{b}(\text{incr}, q_1).q_1 \cdot h(x_1). (\bar{h}\langle x_1 \rangle \\ | \bar{b}(\text{id}, q_2). \\ q_2 \cdot h(x_2). (\bar{h}\langle x_2 \rangle \\ | \bar{p}\langle x_i \rangle)) $$

We first compare the processes

$$ \nu h(\bar{h}\langle 0 \rangle | a(b,p). P_1 | Q_{\text{incr}} | Q_{\text{id}}) \text{ and } \nu h(\bar{h}\langle 0 \rangle | a(b,p). P_2 | Q_{\text{incr}} | Q_{\text{id}}), $$
where $Q_{\text{incr}}$ (resp. $Q_{\text{id}}$) is the encoding of function $\text{incr}$ (resp. $\text{id}$).

Here, the only way to change the value stored in $h$ is by calling $\text{incr}$, which is not visible by the observer after the input on $q_1$. These two processes are bisimilar under any visibility.

Then we compare the processes

$Q_1 \stackrel{\text{def}}{=} \nu h(\bar{h}\langle 0 \rangle | !a(b,p). P_1 | Q_{\text{incr}} | Q_{\text{id}})$ and $Q_2 \stackrel{\text{def}}{=} \nu h(\bar{h}\langle 0 \rangle | !a(b,p). P_2 | Q_{\text{incr}} | Q_{\text{id}})$.

We are able to distinguish them using a re-entrant call :

$$R \stackrel{\text{def}}{=} \bar{a}(b,p). (b(\text{incr}, q). \bar{a}(d,r). (!d(-, s). \overline{\text{incr}}(t). t. \bar{s} \mid r(n). \text{if } n = 1 \text{ then } \bar{q} \text{ else } \omega) \mid p(m))$$

The idea is to call $a$ a second time when $\text{incr}$ is still in the observer's visibility; this means that the new server passed to $a$ has access to $\text{incr}$ during both calls. With the observer $R$, only $Q_2$ will be able to send a success signal. Therefore, for any visibility function $\Gamma$ such that $a \in \Gamma(*)$, $Q_1$ and $Q_2$ are not bisimilar under visibility $\Gamma$.

The processes $Q_1$ and $Q_2$ can be seen as the $\pi$-calculus counterparts of the following ML program. (This example, with re-entrant calls, has been inspired by similar examples in game semantics of functional languages):

```
let h = ref 0 in
let incr () = h := !h +1 in
let id x = x in
let a b =
    b incr;
    let x_1 = !h in
    b id;
    let x_2 = !h in
    x_i
```

These programs can be distinguished by the following ML program that corresponds to the process $R$:

```
let b f =
    let d _ = f () in
    let n = a d in
    if n = 1 then () else \omega
in
a b
```

The idea is the same as before: $d$ calls $f$ which will be $\text{incr}$ in the first call to $b$; therefore at each call to $d$ the reference is incremented. As a consequence, first program returns 1 while the second one returns 2.
## D.2 Typed bisimilarity

**Definition 49 (Typed Bisimulation).** A typed relation $\mathcal{R}$ is a typed (weak) bisimulation if whenever $([\Gamma | \kappa], P, Q) \in \mathcal{R}$:

1. if $[\Gamma | \kappa]P \xrightarrow{\mu} [\Gamma' | \kappa']P'$ then there is $Q'$ such that $[\Gamma | \kappa]Q \xrightarrow{\tilde{\mu}} [\Gamma' | \kappa']Q'$ and $([\Gamma' | \kappa'], P', Q') \in \mathcal{R}$;

2. the converse, on the actions from $Q$.

*Typed bisimilarity*, written $\approx^{}$, is the largest typed bisimulation. For two $\langle\Delta | \sigma\rangle$-processes $P, Q$ we write $P \approx_{\langle\Delta|\sigma\rangle}^{[\Gamma|\kappa]} Q$ when $([\Gamma | \kappa], P, Q) \in \approx^{}$ and $\langle\Delta | \sigma\rangle$ and $[\Gamma | \kappa]$ are compatible.

**Theorem 50 (Soundness of bisimilarity for barbed equivalence).** Suppose $\langle\Delta | \sigma\rangle \vdash P, Q$ with $P \approx_{\langle\Delta|\sigma\rangle}^{[\Gamma|\kappa]} Q$. Then also $P \cong_{\langle\Delta|\sigma\rangle}^{[\Gamma|\kappa]} Q$.

**Theorem 51 (Completeness of bisimilarity for barbed equivalence).** If $P$ and $Q$ are image-finite processes, and if $P \cong_{\langle\Delta|\sigma\rangle}^{[\Gamma|\kappa]} Q$, then $P \approx_{\langle\Delta|\sigma\rangle}^{[\Gamma|\kappa]} Q$.

## D.3 Properties of traces: views and well-bracketing

Along the lines of the material presented in Section 4.2, we can reason about the traces produced by typable processes, based on the notion of justification. For this, we adapt Definition 22 to define views for traces. The notion of *respecting views* (Definition 23) is also adapted straightforwardly, which allows us to obtain the analogue of Lemma 24.

**Lemma 52.** Consider $\Delta, \Gamma, \sigma, \kappa, P$ such that $\langle\Delta | \sigma\rangle \vdash P$ and $[\Gamma | \kappa]$ is compatible with $\langle\Delta | \sigma\rangle$. Let $A = (\Gamma \cup \Delta)(*)$, then every trace of $P$ under $[\Gamma | \kappa]$ respects views with starting visibility $A$.

As highlighted in [3], continuation names allow us to formulate a property of well-bracketing for traces, enforced by our type system. In contrast with [3], however, we do not impose input receptiveness on continuation names.

**Definition 53 (Well-bracketing).** An action of the form $a\langle v\rangle(b, p)$ or $\bar{a}\langle v\rangle(b, p)$ is called a *question*. An action of the form $p\langle v\rangle(b)$ or $\bar{p}\langle v\rangle(b)$ is called an *answer*.

A trace $\mu_1 \dots \mu_n$ is *well-bracketed* if for all $i < j$, if $\mu_i$ is a question and $\mu_j$ is an answer with $\mu_i \not\prec \mu_k$ and $\mu_k \not\prec \mu_j$ for all $i < k < j$, then $\mu_i \prec \mu_j$.

A stack $\sigma$ is *clean* if each name has at most one occurrence, with any tag, in $\sigma$. A trace $\mu_0 \dots \mu_n$ is a *typed trace emanating from $P_0$* if there are $\Delta_1, \sigma_1, \dots, \Delta_n, \sigma_n, P_1, \dots, P_n$ such that for all $0 \le j < n$ we are in one of the cases given by Theorem 27, which gives $\langle\Delta_{j+1} | \sigma_{j+1}\rangle$ when $P_j \xrightarrow{\mu_{j+1}} P_{j+1}$.

**Lemma 54.** Suppose $\langle\Delta_0 | \sigma_0\rangle \vdash P_0$, where $\sigma_0$ is clean. All typed traces emanating from $P_0$ are well-bracketed.