# A Behavioural Theory for a π-calculus with Preorders

Daniel Hirschkoff, Jean-Marie Madiot, Xian Xu

► To cite this version:

Daniel Hirschkoff, Jean-Marie Madiot, Xian Xu. A Behavioural Theory for a π-calculus with Preorders. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. pp.143-158, 10.1007/978-3-319-24644-4_10 hal-01246094v2

HAL Id: hal-01246094

https://inria.hal.science/hal-01246094v2

Submitted on 26 Jan 2017

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# A behavioural theory for a π-calculus with preorders

Daniel Hirschkoff<fnref n="1" />, Jean-Marie Madiot<fnref n="1" />, and Xian Xu<fnref n="2" />

**Abstract.** We study the behavioural theory of πP, a π-calculus in the tradition of Fusions and Chi calculi. In contrast with such calculi, reduction in πP generates a preorder on names rather than an equivalence relation. We present two characterisations of barbed congruence in πP: the first is based on a compositional LTS, and the second is an axiomatisatiation. The results in this paper bring out basic properties of πP, mostly related to the interplay between the restriction operator and the preorder on names.

Consequently, πP is a calculus in the tradition of Fusion calculi, in which both types and behavioural equivalences can be exploited in order to reason rigorously about concurrent and mobile systems.

# 1 Introduction

The π-calculus expresses mobility via name passing, and has two binders: the input prefix binds the value to be received, and restriction is used to delimit the scope of a private name. The study of Fusions [16], Chi [8], Explicit Fusions [20] and Solos [13] has shown that using restriction as the only binder is enough to express name passing. In such calculi (which, reusing a terminology from [10], we shall refer to as *fusion calculi*), the bound input prefix, *c(x)*.P, is dropped in favour of free input, *cb.P*, and communication involving two prefixes *cb* and *ca* generates the *fusion* of names *a* and *b*. This yields a pleasing symmetry between input and output prefixes; moreover, one can encode bound input in terms of free input as $(νx)cx.P$. Fusion calculi therefore promote *minimality* (keep only restriction as a binder) and *symmetry* (input and output prefixes play similar roles). Moreover, and most importantly, fusions act on restricted names, in contrast with the π-calculus, where restricted names can only replace names bound by input (and are thus treated like constants).

The behavioural theory of existing fusion calculi is generally simpler than in the π-calculus (in particular, bisimilarity is a congruence). Fusion calculi have notably been used to analyse concurrent constraints [19], to study distributed implementations of programming languages [9,5] and to establish connections with proof theory [7].

Symmetry comes however at a price. It has indeed been shown in [10] that i/o-types (input/output types, [17]) cannot be adapted to a fusion calculus. Such

<footnote n="1">¹ ENS Lyon, Université de Lyon, CNRS, INRIA, France,</footnote>

<footnote n="2">² East China University of Science and Technology, China</footnote>
types go beyond the simple discipline of sorting, and can be useful, in particular, to reason using typed behavioural equivalences [17,18].

The intuitive reason of the incompatibility of i/o-types with fusions can be explained by considering the following structural congruence law in Explicit Fusions (but the point is essentially the same for other fusion calculi):

$$a(x).P \mid a=b \equiv b(x).P \mid a=b.$$

Process $a=b$ is an explicit fusion. The law says that in presence of $a=b$, an input on $a$ can be viewed as the same input on $b$, and vice-versa (fusion processes are somehow akin to equators, in an asynchronous setting [12]). This shows that fusions define a symmetric relation on names; this is incompatible with a nontrivial (i.e., asymmetric) subtyping relation, which is necessary for i/o-types to make sense.

This observation has led in [10] to the introduction of $\pi P$, a $\pi$-calculus with name preorders. The most important difference between $\pi P$ and existing name-passing calculi is that interaction does not have the effect of equating (or *fusing*) two names, but instead generates an *arc* process, as follows:

$$\bar{c}a.P \mid cb.Q \rightarrow a/b \mid P \mid Q.$$

The arc $a/b$ expresses the fact that anything that can be done using name $b$ can be done using $a$ as well (but not the opposite): we say that $a$ is above $b$. Arcs induce a preorder relation on names, which can evolve along reductions.

Arcs can modify interaction possibilities: in presence of $a/b$, $a$ is above $b$, hence a process emitting on $b$ can also make an output transition along channel $a$. In general, an output on channel $c$ can interact with an input on $d$ provided $c$ and $d$ are joinable, written $c \gamma d$, which means that there is some name that is above both $c$ and $d$ according to the preorder relation. To formalise these observations, the operational semantics exploits conditions involving names, which are either of the form $b \prec a$ ($a$ is above $b$), or $a \gamma b$ ($a$ and $b$ are joinable).

$\pi P$ can be described as a variant of Explicit Fusions, in which arcs replace fusion processes. Beyond the possibility to define i/o-types and subtyping for $\pi P$ [10], we would like to analyse the consequences of the novel aspects of $\pi P$, whose behaviour does not seem to be reducible to existing calculi.

In particular, name preorders have an impact on how processes express behaviours. Barbed congruence for $\pi P$, written $\simeq$, is defined in [10]. Some laws for $\simeq$ suggest that the behavioural theory of $\pi P$ differs w.r.t. existing fusion calculi. As an illustration, consider the following *interleaving law*, which is valid in $\pi P$ (and in $\pi$):

$$\bar{a}(x).\bar{b}(y).(\bar{x} \mid y) \simeq \bar{a}(x).\bar{b}(y).(\bar{x}.y + y.\bar{x}).$$

$\bar{a}(x)$ is the emission of a fresh name $x$ on $a$, and $\bar{x}$ (resp. $y$) stands for an output (resp. input) where the value being transmitted is irrelevant. In Fusions, unlike in the $\pi$-calculus, the process that creates successively two fresh names $x$ and $y$ cannot prevent the context from equating ("fusing") $x$ and $y$. Hence, in order for the equivalence to hold, it is necessary to add a third summand on the right, $[x = y]\tau$. This example suggests that $\pi P$ gives a better control on restricted
names than existing fusion calculi. This issue also motivated the study of two variants of fusion calculi that have a refined notion of restriction [3,4].

The main purpose of the present work is to deepen the study of the behavioural theory of $\pi\mathcal{P}$, in an untyped setting. We define a Labelled Transition System (LTS) for $\pi\mathcal{P}$, and show that the induced notion of bisimilarity, written $\sim$, characterises $\simeq$ (Section 3). It can be noted that [10] presents a characterization of barbed congruence, using an LTS that is rather ad hoc, because it is based on the definition of the reduction relation. Unlike the latter, the LTS we present here is *structural*.

The LTS reveals interesting aspects of interaction in $\pi\mathcal{P}$. An important observation is related to the interplay between arcs and the restriction operator. It is for instance possible for a process to react to an input offer on some channel, say $c$, without being actually able to perform an output on $c$. This is the case for process $P_0 \triangleq (\nu a)(\bar{a}(x).0 \mid a/c)$. Because $a$ is above $c$ in the preorder, $P_0$ cannot do an output on $c$, although $c$ is occurs free in $P_0$ (it could if the arc $a/c$ was replaced with $c/a$). However, $P_0 \mid c(y).0$ can perform a reduction: intuitively, by extending the scope of $(\nu a)$, the input at $c$ can be moved to $a$, so that the communication takes place.

This phenomenon leads to the addition of a new type of labels in the LTS, corresponding to what we call *protected actions*: in the example $P_0$ can do a protected output at $c$, meaning that it can react to an input offer at $c$. Accordingly, we introduce *protected names*, which correspond to (usages of) names where a protected action occurs: intuitively, in $P_0$, name $c$ is protected. As expected, protected actions correspond to observables in the reduction-based semantics supporting the definition of $\simeq$.

Arc processes do not have transitions, but they induce relations between names, which in turn influence the behaviour of processes. Accordingly, strong bisimilarity, $\sim$, not only tests transitions, but also has a clause to guarantee that related processes entail the same conditions.

Finally, the LTS also includes a label $[\varphi]\tau$, expressing “conditional synchronisation”. Intuitively, process $\bar{a} \mid b$ is not able to perform a $\tau$ transition by itself, but it should be when the environment entails $a \gamma b$. Hence, in order for our LTS to be compositional, we include labels of the form $[\varphi]\tau$, interpreted as “$\tau$ under the condition $\varphi$”.

In Section 4, we provide a second characterisation of barbed congruence, by presenting a set of laws that define an axiomatisation of $\simeq$. Algebraic laws help analysing the behaviour of the constructs of the calculus and their interplay. We present a sample of behavioural equalities, and explain how they can be derived equationally, in Section 4.1.

The axiomatisation we give is less simple than, say, the one for Fusions in [16], for two reasons: first, we manipulate preorders between names rather than equivalences. Second, the preorder is explicitly represented in processes, so that some equational laws must describe the interplay between processes and the preorder relation. On the contrary, such aspects are dealt with implicitly in Fusions—we sketch how our ideas can be adapted to Explicit Fusions in Section 4.3.
The axiomatisation exploits the idea that $\pi P$ processes have a state component, corresponding to the preorder induced by arcs. Several laws in the axiomatisation express persistence of the state component (the state can only be extended along computation). Moreover, the restriction operator prevents the state from being globally shared in general: for instance, in process $P_0$ above, name $a$ can be used instead of $c$, but is only known inside the scope of $(\nu a)$. All in all, the handling of restriction in our axiomatisation requires more care than is usually the case, due to the necessity to express the “view” that subprocesses have on the preorder of names.

To present the axiomatisation, we renounce minimality. The syntax of the calculus in this paper differs from the one in [10]: we include bound prefixes and sums with conditions, as it is customary for axiomatisations for the $\pi$-calculus [15,18]. We compare the calculus from [10] with ours in Remark 3 and Proposition 11. We show that the differences are unimportant: the calculus from [10] can be encoded into ours and the behavioural equivalence is unaffected.

We focus in this paper on a finite calculus. This is sufficient to enlighten the main aspects of the behavioural theory of processes. We do not expect any unpredicted difficulty to arise, in the definition of labelled transitions and bisimilarity, from the extension of $\pi P$ with a replication operator.

The paper describes our results and sketches the most important proofs. We refer to [11] for a more detailed presentation of the technical details. Related work is discussed along the paper, where it is relevant.

## 2 $\pi P$: Reduction-Based Semantics

*The Calculus: Preorders and Processes.* We consider a countable set of names $a, b, c, \dots, x, y, \dots$, and define conditions $(\varphi)$, extended names $(\alpha, \beta)$, prefixes $(\pi)$ and processes $(P, Q)$ as follows:

$$ \begin{array}{l} \varphi ::= a \prec b \mid a \succ b \quad \alpha, \beta ::= a \mid \{a\} \quad \pi ::= \alpha(x) \mid \bar{\alpha}(x) \mid [\varphi]\tau \\ P, Q ::= P \mid Q \mid (\nu a)P \mid a/b \mid \sum_{i \in I} \pi_i \cdot P_i \end{array} $$

There are two forms of conditions, ranged over with $\varphi$: $\varphi = a \prec b$ is read “b is above $a$” and $\varphi = a \succ b$ is read “a and b are joinable”. In both cases, we have $n(\varphi) = \{a, b\}$. We explain below how we extend relations $\prec$ and $\succ$ to extended names. When $n(\varphi) = \{a\}$, we say that $\varphi$ is *reflexive*, and abbreviate in this case prefix $[\varphi]\tau$ as $\tau$. Condition $b \prec a$ is ensured by the arc process $a/b$.

In a prefix $\alpha(x)$ or $\bar{\alpha}(x)$, we say that extended name $\alpha$ is in subject position, while $x$ is in object position. As discussed in Section 1, extended names include *protected names*, of the form $\{a\}$, which can be used in subject position only. We call *protected prefix* a prefix where the subject is a protected name. A prefix of the form $[\varphi]\tau$ is called a *conditional* $\tau$, while other prefixes are called *visible*. Bound and free names for prefixes are given by: $\mathbf{bn}([\varphi]\tau) = \emptyset$ and $\mathbf{bn}(\alpha(x)) = \mathbf{bn}(\bar{\alpha}(x)) = \{x\}$, $\mathbf{fn}([\varphi]\tau) = \mathbf{n}(\varphi)$, $\mathbf{fn}(\alpha(x)) = \mathbf{fn}(\bar{\alpha}(x)) = \mathbf{n}(\alpha)$ with $\mathbf{n}(a) = \mathbf{n}(\{a\}) = \{a\}$.

In a sum process, we let $I$ range over a finite set of integers. 0 is the inactive process, defined as the empty sum. We use $S$ to range over sum processes of the
The remainder of the paper is devoted to the presentation of two characterisations of $\simeq$. We first comment on the definition of $\pi_P$ given above.

One could consider an alternative version of reduction, called “eager”, whereby arcs can rewrite prefixes in one step of computation, yielding, e.g., $d/c \mid c(x).P \mapsto d/c \mid d(x).P$. It appears in [10] that the present semantics is more compelling (for instance $a(x).a(y)$ would not be equivalent to $a(x) \mid a(y)$ in the eager version).

**Remark 3 (Encodability of free and protected prefixes).**

In $\pi_P$, arcs act like “instantaneous forwarders”. This allows us to define an encoding $[\cdot]_f$ from a calculus with free prefixes to a calculus with bound prefixes as follows ($x$ is chosen fresh):

$$[ab.P]_f \triangleq a(x).([P]_f \mid x/b) \qquad [\bar{a}b.P]_f \triangleq \bar{a}(x).([P]_f \mid b/x),$$

where $[\cdot]_f$ preserves other operators of the calculi. We return to this encoding below (Proposition 11), and show that it allows us to reflect behavioural equivalence in [10] into our calculus.

We can also encode protected prefixes as follows ($u$ is chosen fresh):

$$[{a}(x).P]_p \triangleq (\nu u)(u/a \mid u(x).[P]_p) \qquad [{\bar{a}}(x).P]_p \triangleq (\nu u)(u/a \mid \bar{u}(x).[P]_p).$$

Although protected prefixes are in some sense redundant, we do not treat them as derived operators, to simplify the presentation (in particular in Section 4).

The results of this paper (Sections 3 and 4) can be adapted to a calculus featuring only free prefixes, and restriction as the only binder, like the calculus of [10]. This yields more complex definitions to handle bound prefixes and protected actions, in particular when defining sum processes. We discuss in [11] a presentation of transitions and bisimilarity based on free prefixes. It can be noted that the axiomatisation of Fusions given in [16] relies only on free input and output, and treats bound prefixes as derived operators. We think that, for $\pi_P$, handling prefixes for bound and protected actions as derived operators would introduce further technical complications that would make the axiomatisation more obscure.

# 3 A Labelled Transition System for $\pi_P$

## 3.1 LTS and Bisimilarity

The LTS defines transitions $P \xrightarrow{\mu} P'$, where the grammar for the labels, $\mu$, is the same as the one for prefixes $\pi$. We comment on the rules, given in Figure 1.

The first two rules correspond to the firing of visible prefixes. The transition involves a fresh name $x$, upon which the participants in a communication “agree”. Name $y$ remains local, via the installation of an arc, according to the directionality of the prefix. (Adopting a rule with no arc installation would yield a more complex definition of $\sim$). The rule for the $[\varphi]\tau$ prefix is self explanatory. The rule describing communication follows the lines of the corresponding rule for $\mapsto$; no arc is installed (but arcs are introduced in the prefix rules).

The three rules mentioning $▷$ are called *preorder rules*. The two preorder rules for visible actions exploit $<$, which is defined for extended names (as we
did for $\Upsilon$ above). Note that the condition involving $\triangleright$ is the same in these two rules. To understand these rules, and the role of protected actions, we recall the basic intuition about arcs: an arc $d/a$ can transform an interaction at $a$ into an interaction at $d$. For instance, from $P \xrightarrow{a(x)} P'$ and $P \triangleright a \prec d$, we can derive $P \xrightarrow{d(x)} P'$. As a consequence, an input at $a$ can synchronise with an output at $b$ if both $a$ and $b$ can be “pulled upwards in the preorder”, using arcs, to some name, say $u$, which is above $a$ and $b$. Observe also that if, like in $P$ above, the input at $a$ is transformed into an input at $d$, then a name $u'$ standing above $d$ and $b$ can be used to let the synchronisation happen (because $u'$ would be above $a$ and $b$).

If, on the contrary, we want to replace, in the input, name $a$ with a name that sits below $a$, say $c$ (like in process $P_0$ from Section 1), we are moving downwards in the preorder. Because of this, the action becomes protected, and we can derive for instance $P_0 \xrightarrow{\{c\}(y)}$, because $\bar{a}(x).0 \mid a/c \triangleright c \Upsilon a$ (and hence $a \prec \{c\}$). By going downwards, we have somehow fixed the channel where the communication occurs (e.g., at $a$ in $Pf_x u_0$). Indeed, it is no longer the case that an output at $b$ can synchronise with the protected input at $c$ whenever some $u$ is above $b$ and $c$, because such $u$ would not necessarily be above $a$ (where the original input takes place) and $b$ in the preorder. For this reason, we can only move further downwards in the preorder, and for instance deduce, from $P_0 \xrightarrow{\{c\}(y)}$, that $P_0 \xrightarrow{\{c_1\}(y)}$ as soon as $c_1 \prec c$ (which implies $\{c\} \prec \{c_1\}$).

The other preorder rule can be used to modify conditional $\tau$s involved in a transition. As an example, let $P_1 \triangleq (\bar{a}(x).Q \mid n/u) \mid (u(y).R \mid n/a)$. Process $P_1$ can perform a $\tau$ transition: the two arcs can, intuitively, let the output at $a$ and the input at $u$ interact at name $n$. Technically, this can be derived by inferring a $\xrightarrow{[a\Upsilon u]\tau}$ transition (from the output on the left and the input on the right), which can then be turned into a $\tau$ transition, exploiting the fact that the whole process entails $a \Upsilon u$. Finally, the congruence rules are as expected.

**Definition 4** (*$\sim$*). A symmetric relation $\mathcal{R}$ is a bisimulation if $P \mathcal{R} Q$ implies:

- If $P \triangleright \varphi$ then $Q \triangleright \varphi$.

- If $P \xrightarrow{\alpha(x)} P'$, with $x \notin \text{fn}(Q)$, then there is $Q'$ such that $Q \xrightarrow{\alpha(x)} Q'$ and $P' \mathcal{R} Q'$; we impose the same condition with $\bar{\alpha}$ instead of $\alpha$.

- If $P \xrightarrow{[\varphi]^\tau} P'$ then there is $Q'$ such that $Q \xrightarrow{[\varphi]^\tau} Q'$ and $P' \mid \varphi \mathcal{R} Q' \mid \varphi$.

Bisimilarity, written $\sim$, is the greatest bisimulation.

This definition can be related to the efficient bisimulation from [20]. In the last clause, we add $\varphi$ in parallel, since the transition is fired only if $\varphi$ is satisfied.

**Remark 5.** Our LTS does not have rules for opening and closing the scope of a restriction. Instead, we rely on arcs in $\pi_P$ to handle scope extrusion. To illustrate this, consider the following $\pi_P$ transition where a private name $c$ is emitted:

$$ \bar{a}(c).P \xrightarrow{\bar{a}(x)} (\nu c)(c/x | P) . $$

Name $x$ is visible in the label, and arc $c/x$ is installed. Through $x$, the environment can affect $c$, so that $\pi_P$ actually *implement* scope extrusion via arcs,
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** LTS for $\pi_P$. Symmetric versions of the two rules involving $|$ are omitted.</figcaption></figure>

without the need to move restrictions. We have:

$$ \begin{aligned} \bar{a}(c).P \mid a(y).Q &\xrightarrow{\tau} (\nu x)((\nu c)(c/x \mid P) \mid (\nu y)(x/y \mid Q)) \\ &\simeq (\nu c)(\nu y)(P \mid c/y \mid Q). \end{aligned} $$

## 3.2 The Characterisation Theorem

**Lemma 6.** If $P \equiv Q$ and $P \triangleright \varphi$ then $Q \triangleright \varphi$.

**Definition 7.** We define a relation $\sqsubseteq^{\varphi}$ between labels as follows: (i) $\alpha_1(x) \sqsubseteq^{\varphi} \alpha_2(x)$ and $\bar{\alpha}_1(x) \sqsubseteq^{\varphi} \bar{\alpha}_2(x)$ when $\varphi = \alpha_2 \prec \alpha_1$, and (ii) $[\varphi_1]\tau\sqsubseteq^{\varphi}[\varphi_2]\tau$ when $\varphi_1, \varphi \vdash \varphi_2$. We write $\sqsubseteq_P$ for the smallest preorder containing all $\sqsubseteq^{\varphi}$ when $P \triangleright \varphi$.

Intuitively, $\eta \sqsubseteq_P \mu$ means that label $\mu$ is less general than $\eta$, given some condition ($\varphi$ above) entailed by $P$. For instance, we have $\{a\}(x) \sqsubseteq_0 a(x)$. This notion is used in the following lemma to reason about transitions of processes.

**Lemma 8.** If $P \xrightarrow{\mu} P'$ and $\eta \sqsubseteq_P \mu$ then $P \xrightarrow{\eta} P'$. Conversely, whenever $P \xrightarrow{\eta} P'$, there exists $\mu$ such that $\eta \sqsubseteq_P \mu$ and $P \xrightarrow{\mu} P'$, of which there is a proof, not bigger than the one for $P \xrightarrow{\eta} P'$, that does not end with a preorder rule.

Congruence for parallel composition is proved using Lemma 8, which gives:

**Lemma 9.** Relation $\sim$ is a congruence.

**Theorem 10 (Characterisation).** $P \simeq Q$ iff $P \sim Q$.

*Proof (Sketch).* The proof follows a standard pattern: soundness is a consequence of Lemma 9. For completeness, we have to show that contexts can express the conditions in the three clauses of Definition 4, and we define accordingly tester
processes. The first clause about $\varphi$ is handled using process $\overline{\alpha \cdot w_1} | \beta \cdot w_2$ where $\alpha$ and $\beta$ are such that $\varphi = \alpha \gamma \beta$. For transitions (second clause), the counterpart of, e.g., $\xrightarrow{[a](x)}$, is given by tester process $\overline{a}(y) \cdot (z/y | \overline{w} | w)$. We use process $\varphi$ for the third clause, since $P \xrightarrow{[\varphi]\tau} Q$ iff $P | \varphi \xrightarrow{\tau} Q | \varphi$. $\square$

As mentioned above, the calculus in [10] is a version of $\pi P$ with prefixes for free input and output, and without the corresponding bound prefixes. Let us call that calculus $\pi P_1$. The encoding $[\cdot]_f$, which we introduced in Remark 3, allows us to embed $\pi P_1$ into $\pi P$ in a faithful way:

**Proposition 11.** $P \simeq_{\pi P_1} Q$ (in $\pi P_1$) iff $[P]_f \simeq [Q]_f$ (in $\pi P$).

The proof of the above result exploits in a crucial way the fact that, although $\pi P_1$ does not feature sums and the $[\varphi]\tau$ prefix, those are not needed to prove the completeness of $\sim$.

# 4 Axiomatisation

## 4.1 Equational Laws for Strong Bisimilarity

**Notations and Terminology.** We use $A$ to range over processes that consist of compositions of $\varphi$ processes only, which we call *preorder processes*. We often view such processes as multisets of conditions. We use notation $A, P$ to denote a process that can be written, *using the monoid laws for parallel composition*, as $A | P$, where $P$ does not contain toplevel arcs. Note that $A$ may contain restrictions, but only those corresponding to the definition of join processes (given in Section 2).

We write $\vdash P = Q$ whenever $P$ and $Q$ can be related by equational reasoning using the laws of Figure 2. We omit the standard laws expressing that $|$ and $+$ obey the laws of commutative monoids, and that $+$ is idempotent. We also omit the laws for equational reasoning (equivalence, substitutivity). We will reason up to these laws in the remainder.

**Comments on the laws.** Before presenting the properties of the axiomatisation, we comment on the laws of Figure 2 and illustrate them on some examples.

As usual, expansion (L1) allows us to rewrite the parallel composition of two sum processes into a sum, the third summand describing synchronisation in $\pi P$.

*Preorders.* Laws L2-L5 express basic properties of relations $\prec$ and $\gamma$, and actually provide an axiomatisation of $\sim$ for preorder processes.

*Prefixes.* Law L6 propagates $\varphi$s in depth, expressing the persistence of condition processes ($\varphi$). Law L7 is the counterpart of the third clause of Definition 4, and describes the outcome of a $[\varphi]\tau$ transition. Similarly, laws L18-L19 correspond to the firing of visible transitions in the LTS (regarding these rules, see also the comments after Proposition 16).
**Expansion law** (we can suppose $x \neq y$, $\mathbf{bn}(\pi_i) \notin \mathbf{fn}(T)$, $\mathbf{bn}(\rho_j) \notin \mathbf{fn}(S)$.)

$$
\text{L1} \quad \underbrace{\sum_i \pi_i \cdot P_i}_{S} \mid \underbrace{\sum_j \rho_j \cdot R_j}_{T} = \sum_i \pi_i \cdot (P_i \mid T) + \sum_j \rho_j \cdot (S \mid R_j) \\
\phantom{\text{L1} \quad \underbrace{\sum_i \pi_i \cdot P_i}_{S} \mid \underbrace{\sum_j \rho_j \cdot R_j}_{T} = \sum_i \pi_i \cdot (P_i \mid T) + \sum_j \rho_j \cdot (S \mid R_j) } \quad \text{when } \alpha \succ \beta \text{ is defined.} \\
\phantom{\text{L1} \quad \underbrace{\sum_i \pi_i \cdot P_i}_{S} \mid \underbrace{\sum_j \rho_j \cdot R_j}_{T} = \sum_i \pi_i \cdot (P_i \mid T) + \sum_j \rho_j \cdot (S \mid R_j) } \quad \text{and } \{\pi_i, \rho_j\} = \{\bar{\alpha}(x), \beta(y)\}
$$

**Laws for preorder processes**

$$
\text{L2} \quad a \prec b \mid b \prec c = a \prec b \mid b \prec c \mid a \prec c \quad \text{L3} \quad a \prec b \mid c \prec b = a \prec b \mid c \prec b \mid a \succ c
$$

$$
\text{L4} \quad a \prec b \mid b \succ c = a \prec b \mid b \succ c \mid a \succ c \quad \text{L5} \quad a \prec a = 0
$$

**Laws for prefixes** (the counterparts of laws L11-L13 for output are omitted)

$$
\text{L6} \quad \varphi, S + \pi.P = \varphi, S + \pi.(\varphi \mid P) \qquad \text{L7} \quad [\varphi]\tau.P = [\varphi]\tau.(\varphi \mid P)
$$

$$
\text{L8} \quad [a \prec a]\tau.P = [b \succ b]\tau.P
$$

$$
\text{L9} \quad [a \succ b]\tau.P = [a \succ b]\tau.P + [a \prec b]\tau.P
$$

$$
\text{L10} \quad [a \succ b]\tau.P = [a \succ b]\tau.P + [b \succ a]\tau.P
$$

$$
\text{L11} \quad a(x).P = a(x).P + \{a\}(x).P
$$

$$
\text{L12} \quad b/a, S + a(x).P = b/a, S + a(x).P + b(x).P
$$

$$
\text{L13} \quad a/b, S + \{a\}(x).P = a/b, S + \{a\}(x).P + \{b\}(x).P
$$

$$
\text{L14} \quad b/a, S + [a \prec c]\tau.P = b/a, S + [a \prec c]\tau.P + [b \prec c]\tau.P
$$

$$
\text{L15} \quad a/b, S + [c \prec a]\tau.P = a/b, S + [c \prec a]\tau.P + [c \prec b]\tau.P
$$

$$
\text{L16} \quad b/a, S + [a \succ c]\tau.P = b/a, S + [a \succ c]\tau.P + [b \succ c]\tau.P
$$

$$
\text{L17} \quad b/a, S + [a \succ c]\tau.P = b/a, S + [a \succ c]\tau.P + [c \prec b]\tau.P
$$

$$
\text{L18} \quad \alpha(y).P = \alpha(x).(\nu y)(x/y \mid P) \quad \text{if } x \notin \mathbf{fn}(P)
$$

$$
\text{L19} \quad \bar{\alpha}(y).P = \bar{\alpha}(x).(\nu y)(y/x \mid P) \quad \text{if } x \notin \mathbf{fn}(P)
$$

**Laws for restriction** (the counterparts of laws L26 and L27 for output are omitted;
$a \prec b \in A^\ddagger$ stands for $a \prec b \in A$ and $a \neq b$, and similarly for $a \succ b$.)

$$
\text{L20} \quad (\nu b)P = (\nu a)(P\{a/b\}) \quad \text{if } a \notin \mathbf{fn}(P) \qquad \text{L21} \quad (\nu c)(\nu d)P = (\nu d)(\nu c)P
$$

$$
\text{L22} \quad P \mid (\nu a)Q = (\nu a)(P \mid Q) \quad \text{if } a \notin \mathbf{fn}(P) \qquad \text{L23} \quad (\nu a)0 = 0
$$

$$
\text{L24} \quad (\nu a)A = \{b \prec c \mid b \prec a, a \prec c \in A^\ddagger\} \uplus \{b \succ c \mid b \prec a, c \prec a \in A^\ddagger\} \\
\phantom{\text{L24} \quad (\nu a)A = \{b \prec c \mid} \uplus \{b \succ c \mid a \succ c, b \prec a \in A^\ddagger\} \uplus \{\varphi \in A \mid a \notin \mathbf{n}(\varphi)\}
$$

$$
\text{L25} \quad (\nu a)(A, S + \pi.P) = (\nu a)(A, S + \pi.(\nu a)(A \mid P)) \quad a \notin \mathbf{n}(\pi)
$$

$$
\text{L26} \quad (\nu a)(A, S + a(x).P) = (\nu a)(A, S + \sum_{a<b \in A^\ddagger} b(x).(\nu a)(A \mid P) \\
\phantom{\text{L26} \quad (\nu a)(A, S + a(x).P) = (\nu a)(} + \sum_{\begin{subarray}{c} b<a \in A^\ddagger \\ \lor a \succ b \in A^\ddagger \end{subarray}} \{b\}(x).(\nu a)(A \mid P))
$$

$$
\text{L27} \quad (\nu a)(A, S + \{a\}(x).P) = (\nu a)(A, S + \sum_{b<a \in A^\ddagger} \{b\}(x).(\nu a)(A \mid P))
$$

$$
\text{L28} \quad (\nu a)(A, S + [a \prec c]\tau.P) = (\nu a)(A, S + \sum_{a<b \in A^\ddagger} [b \prec c]\tau.(\nu a)(A \mid P)) \quad a \neq c
$$

$$
\text{L29} \quad (\nu a)(A, S + [c \prec a]\tau.P) = (\nu a)(A, S + \sum_{b<a \in A^\ddagger} [c \prec b]\tau.(\nu a)(A \mid P)) \quad a \neq c
$$

$$
\text{L30} \quad (\nu a)(A, S + [a \succ c]\tau.P) = (\nu a)(A, S + \sum_{\substack{a<b \in A^\ddagger \\ \lor a \succ b \in A^\ddagger}} [b \succ c]\tau.(\nu a)(A \mid P)) \quad a \neq c \\
\phantom{\text{L30} \quad (\nu a)(A, S + [a \succ c]\tau.P) = (\nu a)(} + \sum_{\substack{b<a \in A^\ddagger \\ \lor a \prec b \in A^\ddagger}} [c \prec b]\tau.(\nu a)(A \mid P))
$$

<caption>**Fig. 2.** An axiomatisation of ~</caption>
α-conversion for input prefixes follows from laws L20 and L18, by deriving the following equalities (and similarly for the other visible prefixes):

$$a(y).P \stackrel{L18}{=} a(x).(\nu y)(x/y | P) \stackrel{L20}{=} a(x).(\nu y')(x/y' | P\{y'/y\}) \stackrel{L18}{=} a(y').P\{y'/y\}.$$

Laws L11-L17 can be used to expand process behaviours using the preorder: arcs can modify the subject of visible prefixes (L11-L13) and the condition in $[\varphi]\tau$ prefixes (L14-L17). Laws L9, L10 and L14-L17 rely on the defining properties of relations $\prec$ and $\succ$. Finally, law L8 is used to equate all reflexive $\tau$ prefixes.

**Restriction.** Laws L20-L23 are standard. The other laws are used to “push” restrictions inside processes. Due to the necessity to handle the preorder component (A), they are rather complex.

Law L24 is used to eliminate a restriction on a name a in a preorder process, by propagating the information expressed by all $\varphi$s that mention a.

Law L25 is rather self-explanatory, and shows how the A component prevents us from simply pushing the restriction downwards (under prefixes).

Laws L26-L30 describe a kind of “synchronous application” of the prefix laws seen above. For instance, the two summands in law L26 correspond to applications of laws L12-L13: as we push the restriction on a downwards, we make sure that all possible applications of these laws are taken into account.

Intuitively, L24 is applied after laws L25-L30 have been used to erase all prefixes mentioning the restricted name a, pushing the restriction on a inwards.

All in all, the set of laws in Figure 2 is rather lengthy. We make two comments on this. First, it can be remarked that axiomatisations often treat restriction separately, by first focusing on a restriction-free calculus. In $\pi_P$, because of preorder processes, we cannot in general push restrictions on top of sum processes, so the situation is more complex (see also the discussion about [14] in Section 5).

Second, we could have presented the laws in a more compact way, by writing schemas. A uniform presentation for laws L8-L17 and L26-L30 is as follows:

$$\frac{\eta \sqsubseteq_A \mu \quad \mu.P \in S}{A, S = A, S + \eta.P} \qquad \frac{a \in \mathit{fn}(\mu) \quad \forall \eta \sqsubseteq_A \mu \quad a \in \mathit{fn}(\eta) \lor \exists \rho \quad \eta \sqsubseteq_A \rho \land \rho.P \in S}{(\nu a)(A, \mu.P + S) = (\nu a)(A, S)}$$

(To remove $\mu.P$ from $\mu.P + S$, the second rule requires that some $\rho.P$ are in S. The second rule can be used to add those summands to S.) We prefer nevertheless to write all rules explicitly, since this is how they are handled in proofs.

**Examples of derivable equalities.** In the following examples, we sometimes switch silently to notation A, P to ease readability. We also allow ourselves to simplify some reasonings involving prefixes where the object is not important. We explain how the following derivable between $\pi_P$ processes can be derived:

$$\begin{align*}
(\nu a)(b/a \mid a/c) &= b/c & (\nu a)(S+a(x).P) &= (\nu a)S \\
(\nu a)(a/b \mid a(x).P) &= \{b\}(x).(\nu a)P & \bar{a}(x).x &= \bar{a}(x).\{x\} & a(x).\{x\} &= a(x).0
\end{align*}$$
The first equality above is established using law L24: before getting rid of the restriction on $a$, we compute all conditions not involving $a$ that can be deduced from $b/a$ | $a/c$. In this case, this is only $b/c$.

The second equality is a direct consequence of law L26. Law L26 is also used for the third equality: only the second sum in the law is not empty, which gives $(\nu a)(a/b, a(x).P) = (\nu a)(a/b, \{b\}(x).(\nu a)P)$. Then, L22 allows us to restrict the scope of $\nu a$, and we can get rid of $(\nu a)a/b$ using law 24, which yields the result.

Another way to see the third equality is to observe that we can derive $a/b, a(x).P = a/b, a(x).P + \{a\}(x).P + \{b\}(x).P$ using laws L11 and L13. In the latter process, the sum is intuitively *expanded*, in the sense that all derivable toplevel summands have been made explicit. When considering the restricted version of both processes, it is sound to push the restriction on $a$ downwards in the expanded process, to obtain the expected equality. In this sense, law L26 implements a “synchronous version” of this reasoning, so as to insure that when pushing a restriction downwards, the behaviour of the process is fully expanded.

The next two equalities illustrate the meaning of protected names. We reason as follows: $\bar{a}(x).x \stackrel{L19}{\equiv} \bar{a}(x').(\nu x)(x/x', x) \stackrel{L26}{\equiv} \bar{a}(x').(\nu x)(x/x', \{x'\}).(\nu x)(x/x' | 0)$. We then obtain the expected equality by getting rid of $(\nu x)x/x'$, twice, using laws L22 and L24. The reason why this equality holds is that fresh name $x$ is emitted without the context having the ability to interact at $x$, since $x$ will never be under another name in an arc. Therefore, the input at $x$ is equivalent to a protected input.

In the last equality, because of the transition $a(x).\{x\} \stackrel{a(x')}{\longrightarrow} (\nu x)(x'/x | \{x\})$, $x$ will never be above another name, so that the prefix $\{x\}$ cannot be triggered, and is equivalent to 0. This equality is derived as follows:

$$a(x).\{x\} \stackrel{L18}{\equiv} a(x').(\nu x)(x'/x | \{x\}) \stackrel{L27}{\equiv} a(x').(\nu x)x'/x \stackrel{L24}{\equiv} a(x').0 .$$

(we have explained above how $a(x').0 = a(x).0$ can be derived).

We leave it to the reader to check that the law for interleaving, presented in Section 1, can be derived using the expansion law, followed by the rules for prefixes and restriction to get rid of the summand $[x \upharpoonright y]\tau.(\nu t, u)(t/u)$.

## 4.2 Soundness and Completeness of the Axioms

**Lemma 12 (Soundness).** *The laws of Figure 2 relate bisimilar processes.*

*Proof (Sketch).* For laws 24-30, we establish a “saturation property”, expressing the fact that when erasing a preorder process $\varphi$ or a prefix $\pi$ that mentions $a$, we generate all processes $\varphi$ or $\pi$ could induce. The other laws are easy. $\square$

**Auxiliary Results: Preorder Processes, Prefixes, Restriction.**

In order to establish completeness, we first need some technical results, given by Propositions 13, 16 and 17.

First, laws L2-L5 can be used to *saturate* preorder processes:
**Proposition 13.** If $A_1, S_1 \sim A_2, S_2$, then there exists $A^*$ such that $\vdash A_i, S_i = A^*, S_i$ ($i = 1, 2$), and $A^* = \coprod \{\varphi \mid \varphi \text{ not reflexive and } A_1 \succcurlyeq \varphi\}$.

(Note that we could have picked $A_2$ instead of $A_1$ above.) We say that $A$ is a saturated preorder process whenever $A^* \equiv A$. We use $A^*$ to range over such processes. We can remark that even if $A$ contains only arcs, $A^*$ may contain restrictions, because of induced conditions involving $\Upsilon$.

The next lemma relates transitions of sum processes and the laws for prefixes.

**Lemma 14.** If $A, S \xrightarrow{\mu} A, P$ then $\vdash A, S = A, S + \pi.Q$ for some $\pi$ and $Q$ such that $\mu$ and $\pi$ only differ in their bound names and $\pi.Q \xrightarrow{\mu} P$.

Laws L9-L17 can be used to “saturate” the topmost prefixes in sums. We express this using the equivalence below, and rely on Lemma 14 to prove Prop. 16:

**Definition 15 (Head sum normal form, $\asymp_h$).** Given two sum processes $S$ and $T$, we write $S \prec_h T$ whenever for any summand $\pi.P$ of $S$, there exists a summand $\pi.Q$ of $T$ with $\pi.P \sim \pi.Q$. We let $S \asymp_h T$ stand for $S \prec_h T \wedge T \prec_h S$.

**Proposition 16.** Whenever $A^*, S_1 \sim A^*, S_2$, where $S_1, S_2$ are two sum processes, there are $S'_1, S'_2$ s.t. $\vdash A^*, S_i = A^*, S'_i$ ($i = 1, 2$) and $S'_1 \asymp_h S'_2$.

In the definition of $\prec_h$, we impose $\pi.P \sim \pi.Q$, and not simply $P \sim Q$. The equivalence induced by the choice of the latter condition would indeed be too discriminating. To see why, consider $Q_1 = a(x).c/x$ and $Q_2 = a(x).0$. Obviously, $c/x \not\sim 0$. On the other hand, we have $Q_1 \sim Q_2$: after a $\xrightarrow{a(y)}$ transition on both sides, we must compare $(\nu x)(c/x \mid y/x)$ and $(\nu x)(y/x)$, and both are bisimilar to 0. In order to derive $\vdash Q_1 = Q_2$, we rely on the following property, which explains the shape of laws L18, L19: $a(y).P \sim a(y).Q$ iff $(\nu y)(x/y \mid P) \sim (\nu y)(x/y \mid Q)$.

Proposition 17 expresses that restrictions can be pushed inwards in processes. It introduces a notion of measure on processes that is useful to reason by induction on processes in the completeness proof:

**Proposition 17.** We define $|P|$ as follows: $|\sum_i \pi_i.P_i| = \max_i (1 + |P_i|) |(\nu a)P| = |P|$, $|P| |Q| = |P| + |Q|$, and $|a/b| = 0$.

For any $A, S, a$, there exist $A'$ and $S'$ such that $\vdash (\nu a)(A, S) = A'$, $S'$ and $|(\nu a)(A, S)| \ge |A'|, |S'|$.

**Establishing Completeness.** The grammar $P ::= A, \sum_i \pi_i.P_i \mid (\nu a)P$ defines what we call *|-free processes*: only arcs are composed, and the non-preorder part of processes is a sum.

**Proposition 18.** For all *|-free processes* $P$ and $Q$, $P \sim Q$ iff $\vdash P = Q$.

*Proof (Sketch).* The ‘if’ part follows from Lemmas 9 and 12. Suppose now $P \sim Q$; we reason by induction on $|P| + |Q|$. By Propositions 17, 13 and 16, we obtain $\vdash P = A^*, S_1$ and $\vdash Q = A^*, S_2$, for some $A, S_1, S_2$ such that $S_1 \asymp_h S_2$.
We then consider $a(x).T_1 \in S_1$ and $a(x).T_2 \in S_2$ s.t. $a(x).T_1 \sim a(x).T_2$. The latter yields, by triggering the input transition, $(\nu x)(y/x | T_1) \sim (\nu x)(y/x | T_2)$. By induction we derive $\vdash (\nu x)(y/x | T_1) = (\nu x)(y/x | T_2)$ from which we get $\vdash a(x).T_1 = a(x).T_2$ by law L18.

The other kinds of prefixes are handled similarly. This reasoning allows us to prove $\vdash S_1 = S_2$ and hence $\vdash P = Q$. $\square$

The expansion law yields the following result, which then gives Theorem 20.

**Lemma 19.** For any $P$, there exists a $|-\text{free process } Q$ s.t. $\vdash P = Q$.

**Theorem 20 (Axiomatisation of $\sim$).** For all $P$ and $Q$, $P \sim Q$ iff $\vdash P = Q$.

*Remark 21 (Normal forms).* The proofs of the results in this section suggest that we can define a strategy to apply the rules of Figure 2, in order to rewrite a $\pi_P$ process $P$ to its normal form, $nf(P)$, so that $P \sim Q$ iff $nf(P) = nf(Q)$. We leave the rigorous description of this normalisation procedure for future work.

## 4.3 Adapting our Axiomatisation to Explicit Fusions

We can reuse the ideas presented above to describe an axiomatisation for barbed congruence in Explicit Fusions (EF, [20]). EF feature fusion processes, of the form $a=b$, which can equate names via $\equiv$: we have $a=b | P \equiv a=b | P\{b/a\}$.

Like in $\pi_P$, we work with three kinds of prefixes, $\bar{a}(x)$, $a(x)$ and $[a=b]\tau$, the latter being the counterpart of $[\varphi]\tau$ in $\pi_P$ (it appears, e.g., in [20]).

The “state component” of processes is simpler in EF than in $\pi_P$, since fusions implement an equivalence relation on names. The laws of Figure 2 can be ported to EF, yielding an axiomatisation. We only discuss some relevant laws, and refer to [11] for a complete definition. The laws for fusion processes are

$$a=a=0 \qquad a=b | a=c = a=b | a=c | b=c \qquad a=b = b=a,$$

and the EF counterpart of (some of) the laws for prefixes in $\pi_P$ is given by

$$a=b | a(x).P = a=b | b(x).P \qquad a=b | [a=c]\tau.P = a=b | [b=c]\tau.P$$

(laws L6-L7 are inherited directly, $\varphi$ denoting fusions). Because fusions satisfy transitivity, every fusion can be eliminated if one of its names is restricted, as $(\nu a)(a=b | P) \sim P\{b/a\}$. This makes the laws for restriction much simpler than in $\pi_P$:

$$(\nu a)a=b = 0 \qquad (\nu a)\sum_i \pi_i.P_i = \sum_{i|a \notin n(\pi_i)} \pi_i.(\nu a)P_i.$$

## 5 Conclusions and Future Work

Working with a preorder on names has an influence on the behavioural theory of $\pi_P$, notably through the interplay between arcs and restrictions. The preorder relation is represented explicitly in $\pi_P$ processes, using arcs. We do not see any natural “implicit version” of $\pi_P$, mimicking the relation between Explicit Fusions and Fusions, whereby the extension of the preorder along a communication would not generate an arc process.
The stateful nature of the preorder component of $\pi P$ processes can be related to frames in the applied $\pi$-calculus [1] and Psi-calculi [2]. Arcs in $\pi P$ can be seen in some sense as substitutions, but they differ from the active substitutions of applied $\pi$. The latter map variables to terms, while, in the tradition of fusion calculi, we only have (channel) names in $\pi P$. Moreover, several arcs acting on the same name are allowed in $\pi P$, while a substitution acts on at most one variable in applied $\pi$. For these reasons, the behavioural theories of $\pi P$ and applied $\pi$ are rather different. Liu and Lin's proof system for applied $\pi$ [14] departs from our axiomatisation for $\pi P$, but has in common the stateful component of processes.

Psi-calculi can represent the active substitutions of applied $\pi$. It would be interesting to study whether arcs, and the preorder between names, can be represented in the setting of Psi-calculi. An important technical point to address in this perspective is whether transitivity of (generalised) channel equivalence in Psi-calculi would conflict with the fact that name joinability is not transitive in $\pi P$. Another important feature of Psi-calculi is that they come with a fully mechanised metatheory: this is clearly something that $\pi P$ is lacking at the moment.

The behavioural theory of $\pi P$ is based on an operational account. An intriguing question is the construction of a denotational model for $\pi P$, and the comparison with known models for $\pi$ and Fusions. We would also like to study the weak version of behavioural equivalence.

The results of this work provide foundations for the behavioural theory of the $\pi P$ calculus, which also has i/o-types (cf. [10]). As already mentioned, typed behavioural equivalence [17,6] can be used to establish fine behavioural properties of concurrent systems. We would like to find out whether it can be helpful to refine untyped analyses of systems where Fusions have been used.

***Acknowledgements.*** We thank Davide Sangiorgi and Fu Yuxi for useful discussions about this work. This work has been supported by projects ANR 12IS02001 PACE, ANR 2010-BLAN-0305 PiCoq and NSF of China (61261130589).

## References

1. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In *Proc. of POPL*, pages 104–115. ACM, 2001.

2. J. Bengtson, M. Johansson, J. Parrow, and B. Victor. Psi-calculi: Mobile processes, nominal data, and logic. In *LICS*, page 39–48. IEEE, 2009.

3. M. Boreale, M. G. Buscemi, and U. Montanari. D-fusion: A distinctive fusion calculus. In *Proc. APLAS*, volume 3302 of *LNCS*, pages 296–310. Springer, 2004.

4. M. Boreale, M. G. Buscemi, and U. Montanari. A general name binding mechanism. In *Proc. TGC*, volume 3705 of *LNCS*, pages 61–74. Springer, 2005.

5. S. Carpineti, C. Laneve, and L. Padovani. PiDuce - A project for experimenting Web services technologies. *Sci. Comput. Program.*, 74(10):777–811, 2009.

6. Y. Deng and D. Sangiorgi. Towards an algebraic theory of typed mobile processes. *Theor. Comput. Sci.*, 350(2-3):188–212, 2006.

7. T. Ehrhard and O. Laurent. Acyclic solos and differential interaction nets. *Logical Methods in Computer Science*, 6(3), 2010.

8. Y. Fu. The $\chi$-calculus. In *APDC*, pages 74–81. IEEE Computer Society, 1997.
9. P. Gardner, C. Laneve, and L. Wischik. The fusion machine. In *CONCUR*, volume 2421 of *Lecture Notes in Computer Science*, pages 418–433. Springer, 2002.

10. D. Hirschkoff, J.-M. Madiot, and D. Sangiorgi. Name-passing calculi: From fusions to preorders and types. In *LICS*, pages 378–387. IEEE Computer Society, 2013.

11. D. Hirschkoff, J.-M. Madiot, and X. Xu. Long version of this paper. Available from http://madiot.org.

12. K. Honda and N. Yoshida. On reduction-based process semantics. *Theor. Comp. Sci.*, 152(2):437–486, 1995.

13. C. Laneve and B. Victor. Solos in concert. *Mathematical Structures in Computer Science*, 13(5):657–683, 2003.

14. J. Liu and H. Lin. Proof system for applied pi calculus. In *Proc. IFIP TCS*, volume 323 of *IFIP Advances in Inf. and Comm. Technol.*, pages 229–243. Springer, 2010.

15. J. Parrow and D. Sangiorgi. Algebraic theories for name-passing calculi. *Inf. Comput.*, 120(2):174–197, 1995.

16. J. Parrow and B. Victor. The fusion calculus: expressiveness and symmetry in mobile processes. In *LICS*, pages 176–185. IEEE, 1998.

17. B. C. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. *Mathematical Structures in Computer Science*, 6(5):409–453, 1996.

18. D. Sangiorgi and D. Walker. *The Pi-Calculus: a theory of mobile processes*. Cambridge University Press, 2001.

19. B. Victor and J. Parrow. Concurrent constraints in the fusion calculus. In *Proc. ICALP*, volume 1443, pages 455–469, 1998.

20. L. Wischik and P. Gardner. Strong bisimulation for the explicit fusion calculus. In *Proc. of FoSSaCS*, volume 2987 of LNCS, pages 484–498, 2004.