Daniel Hirschkoff

Enguerrand Prebet

Davide Sangiorgi

On sequentiality and well-bracketing in the π-calculus

The π-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected.

In this paper we focus on two such common disciplines: sequentiality, meaning that at any time there is a single thread of computation, and well-bracketing, meaning that calls to external services obey a stack-like discipline. We formalise the disciplines by means of type systems. The main focus of the paper is on studying the consequence of the disciplines on behavioural equivalence. We define and study labelled bisimilarities for sequentiality and well-bracketing. These relations are coarser than ordinary bisimilarity. We prove that they are sound for the respective (contextual) barbed equivalence, and also complete under a certain technical condition.

We show the usefulness of our techniques on a number of examples, that have mainly to do with the representation of functions and store.

I. INTRODUCTION

The π-calculus has been advocated as a model to give semantics to, and reason about, various forms of programming languages, including those with higher-order features. Strengths of the π-calculus are its rich algebraic theory and its wide spectrum of proof techniques. Concurrency is at the heart of the π-calculus: computation is interaction between concurrent processes. The operators of the calculus are simple (parallelism, input, output, restriction being the main ones) and unconstrained. This yields an amazing expressive powerthe calculus can model a variety of programming idioms [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]. However, this also makes the contexts of the calculus very discriminating; as a consequence, behavioural equivalences, which are supposed to be preserved by all the contexts of the calculus, are rather demanding relations.

Higher-level languages may be syntactically quite different from a language for pure concurrency such as the π-calculus. For instance, the paradigmatic higher-order programming language, the λ-calculus, is a pure calculus of functions and, in both its call-by-name and call-by-value variants, is sequential -it is even deterministic. A variety of extensions of it have been considered; examples of additional features are references, control operators, non-determinism, (constrained) forms of concurrency. The specific set of syntactic features chosen for the language determines the ways in which the contexts of the language may interact with the terms. In any case, the patterns of interaction are usually more disciplined than those that arise in π-calculus representations of those terms. Thus there are λ-terms that are indistinguishable within the (pure) λ-calculus whose π-calculus images can be separated by appropriate π-contexts.

A well-known way of imposing a discipline to the πcalculus is to equip it with a type system. Such systems are intended to capture communication patterns that occur frequently when programming in the π-calculus. A number of type systems have been considered: e.g., capability types (formalising the intended I/O usage of names that are exchanged among processes), linearity (formalising the property that certain names may be used at most once), session types (formalising the communication protocols in the dialogues between two or more processes), and so on [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF], [START_REF] Kobayashi | Linearity and the picalculus[END_REF], [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF], [START_REF] Ancona | Behavioral types in programming languages[END_REF]. Type systems have also been designed to capture specific properties of processes, such as termination, deadlock-freedom, lockfreedom [START_REF] Kobayashi | A partially deadlock-free typed process calculus[END_REF], [START_REF]A type system for lock-free processes[END_REF], [START_REF] Deng | Ensuring termination by typability[END_REF], [START_REF] Yoshida | Strong normalisation in the pi -calculus[END_REF], [START_REF] Kobayashi | A hybrid type system for lock-freedom of mobile processes[END_REF]. Types impose constraints on the set of legal contexts in which well-typed terms are supposed to be used; this can make behavioural equivalences usefully coarser.

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. Typically this is investigated in the coinductive setting of bisimilarity, and achieved by refining and/or modifying the standard bisimilarity clauses so to take the usage of types into account. The resulting bisimilarity should be sound with respect to contextually-defined forms of bisimilarity such as barbed equivalence (or congruence); ideally, it should also be complete.

In barbed equivalence, the bisimulation game is played only on internal actions, and certain success signals, the barbs, are used to monitor the computation. In the standard barbed equivalence, an arbitrary context may be added, once (at the beginning), on top of the tested processes. In reduction-closed barbed equivalence [START_REF] Honda | On reduction-based process semantics[END_REF], [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF], the context may be dynamically updated, by adding further components during the computation. Reduction-closed barbed equivalence usually allows simpler proofs of completeness, and does not require any hypothesis of image-finiteness on the state space of the tested processes. In contrast, standard barbed equivalence is more robust -reduction-closed barbed equivalence may sometimes be over-discriminating [START_REF] Sangiorgi | Some results on barbed equivalences in pi-calculus[END_REF].

In this paper we focus on the π-calculus representation of sequentiality and well-bracketing. 'Sequentiality' intuitively 978-1-6654-4895-6/21/$31.00 ©2021 IEEE indicates the existence of a single thread of computation. 'Well-bracketing' is a terminology borrowed from game semantics, and used to refer to a language without control operators, in which the call-return interaction behaviour between a term and its context follows a stack discipline. Our main objectives are to define bisimilarity-based proof techniques for type systems in the π-calculus that formalise the sequentiality and well-bracketing notions. We actually work with the asynchronous π-calculus, Aπ, as this is the calculus that is usually adopted in the literature for modelling higherorder languages.

In Aπ, sequentiality is the property that, at any time, at most one process is active, or carries the thread; that is, the process has the control on the computation and decides what the next computation step can be. In other words, we never find two sub-components of a system both of which contain an interaction redex (a pair of an input and an output processes at the same name).

In the (standard) encodings of the λ-calculus [START_REF] Milner | Functions as processes[END_REF], [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF], a process is active, i.e., it carries the thread, when it contains an unguarded output particle. Indeed, the π-calculus terms obtained from the encodings give rise to computations in which, syntactically, at any time there is at most one unguarded output particle. An input process that consumes that output will in turn become active.

Our type system is more general, in that we allow also input processes to carry the thread. The type system specifies whether a name may carry the thread in output or in input; we call these names output-controlled and input-controlled. While the output-controlled are the most important ones (for instance, they play a central role in the modelling of functions), input-controlled names may be useful too, for instance, in the representation of references or locks. A reference that contains the value n is represented in Aπ by an output particle n ; and a process accessing the reference will do so by performing an input at . Thus an input at indicates ownership of the current computation thread.

As remarked above, sequentiality implies absence of parallel computation threads. Sequentiality however does not exclude non-determinism. An output particle a b that owns the thread may have the possibility of interacting with different input processes at a (and symmetrically for input processes owning the thread). Indeed we also admit internal non-determinism (i.e, processes such as τ . P + τ . Q that may chose to reduce either to P or to Q without interactions with the environment), both in active and in inactive processes.

The type system for well-bracketing is a refinement of that for sequentiality, in which a stack of continuation names keeps track of the structure of calls and returns among the processes. These stacks are similar to those used in the implementation of compilers for languages (or fragments of languages) adopting well-bracketing, or used in well-bracketed forms of game semantics.

Finding proof techniques to reason about sequentiality and well-bracketing presents a number of caveats, that have mainly to do with the soundness and completeness of the resulting bisimilarity with respect to barbed equivalence. We briefly discuss below a couple of issues concerning completeness.

In the proof of completeness one has to show that the contexts of the language are at least as discriminating as the labelled bisimilarity. In standard proofs, one defines special contexts that interact with the tested processes and, at the same time, emit certain signals to the outside so to provide information on the kind of interactions that have occurred with the processes. Such behaviour of the testing contexts is however inherently concurrent -the context has to interact with the tested processes and, at the same time, emit signals to the outside -and is therefore liable to break the typing discipline for sequentiality (and hence also well-bracketing).

Further problems arise in proofs about reduction-closed barbed equivalence. The reason why completeness proofs for reduction-closed barbed equivalence may be simpler than with standard barbed equivalence is that the testing context may be incrementally adjusted, after every interaction step with the tested processes. This however requires the existence of special components in the contexts to handle the fresh names generated by the tested processes. Specifically, the task of these components is to ensure that new pieces of contexts, added later, will be able to access such fresh names. Again, these components represent parallel threads, and break the sequentiality and well-bracketing disciplines. For this reason in the paper we cannot appeal to reduction-closed forms of barbed equivalence, remaining within the standard notions and therefore requiring an image-finiteness condition.

In the case of well-bracketing the problems above are enhanced by the presence of continuation names. These names are linear [START_REF] Kobayashi | Linearity and the picalculus[END_REF] (they may only be used once), input receptive [START_REF]The name discipline of uniform receptiveness[END_REF] (the input-end of the name should always be available), and output-controlled. This places further constraints on the use of such names within contexts that test the processes.

For the above reasons, the completeness proofs for sequentiality and well-bracketing present significant technical differences, both between them and from completeness proofs in the literature.

In the paper we propose labelled bisimilarities that allow us to reason about processes following the sequentiality or well-bracketing disciplines. We prove that the bisimilarities are sound with respect to barbed equivalence. We also establish completeness, on processes with only output-controlled names. We do not know whether completeness holds in the general case, with also input-controlled names. We also study some refinements of the bisimilarities: one is obtained by injecting ideas from bisimilarities for calculi with references [START_REF] Hirschkoff | On the representation of references in the pi-calculus[END_REF]; other refinements are forms of 'up-to techniques'. We illustrate applications of our techniques on a number of examples, most of which have to do with the representation of functions and references. Usually the examples are about equalities that only hold under the sequentiality or well-bracketing disciplines; other examples show that sequentiality and well-bracketing may make equalities simpler to prove because there are fewer observables to take into account.

Paper outline. We introduce some background in Section II.

We study sequentiality in Section III, and well-bracketing in Section IV: in each case, we present our type system, define an appropriate notion of bisimilarity, and show some examples or laws that we can derive. Related and future works are discussed in Section V. For lack of space, some technical definitions and proofs are given in [START_REF]On sequentiality and well-bracketing in the π-calculus[END_REF].

II. BACKGROUND: THE (ASYNCHRONOUS) π-CALCULUS

We recall here the standard syntax of the asynchronous πcalculus, Aπ, from [START_REF] Amadio | On bisimulations for the asynchronous pi-calculus[END_REF]:

P, Q ::= a b !a( b). P P | Q (νa)P G G, G ::= 0 a( b). P τ . P [a = b]G G + G
Names are ranged over by a, b, . . .. In prefixes a b and a( b). P , name a is the subject and b are the objects. We use a tilde, like in b, for (possibly empty) tuples of names; similarly (ν a)P stands for a sequence of restrictions. As usual, we write a. P and a when the object of a prefix is the empty tuple. We use i∈I G i (resp. = ⇒, are standard and are given in [START_REF]On sequentiality and well-bracketing in the π-calculus[END_REF]. We note fn(P ) (resp. fn(µ)) the set of free names of P (resp. µ). We sometimes abbreviate reductions P τ -→ P as P -→ P . 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 [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF], in which names are partitioned into a collection of types (or sorts), and a sorting function maps types onto types. If a name type S is mapped onto a type T , this means that names in S may only carry names in T . We assume that there is a sorting system under which all processes we manipulate are well-typed. We write ∆ P when process P is well-typed under ∆, and similarly for other objects, such as contexts.

i∈I P i ) for G i1 + • • • + G in (
The reference behavioural equivalence for us will be the context-closure of barbed bisimulation. We focus on barbed equivalence (as opposed to barbed congruence) because it is simpler (notably, we do not need to consider issues of closure of the labelled bisimulations under name substitutions). The definition of barbed bisimulation uses the reduction relation =⇒ along with an observation predicate ⇓ a for each name a, which detects the possibility of performing an output to the external environment along a. Moreover, since we work in a typed setting, such an output should be allowed by the typing of the tested processes. Thus, we write ∆ P ⇓ a if ∆ is a typing for P (i.e., ∆ P holds), there is an output µ with subject a s.t. P µ =⇒ P , and such a transition is observable under the typing ∆. The meaning of 'observable under a typing' will depend on the specific type system adopted; in the case of the plain sorting, all transitions are observable.

Having typed processes, in the definition of barbed equivalence we may only test processes with contexts that respect the typing of the processes.

Definition 1. C is a Γ/∆ context if Γ C holds,

using the typing for the processes plus the rule ∆ [•]

for the hole.

Similarly, P is a ∆-process if ∆ P . We assume (as in usual Subject-Reduction properties for type systems) that typing is invariant under reduction.

Definition 2 (Barbed bisimulation, equivalence, and congruence). Barbed ∆-bisimulation is the largest symmetric relation .

≈ ∆ on ∆-processes s.t. P . ≈ ∆ Q implies:
1) whenever P -→ P then there exists

Q such that Q =⇒ Q and P . ≈ ∆ Q ; 2) for each name a, ∆ P ⇓ a iff ∆ Q ⇓ a . Two ∆-processes P and Q are barbed equivalent at ∆, written P ∆ Q, if for each Γ/∆ static context E it holds that E[P ] . ≈ Γ E[Q]. Barbed congruence at ∆, ∼ = ∆ , is defined
in the same way but employing all Γ/∆ contexts (rather than only the static ones).

Barbed equivalence in the plain (untyped) Aπ, , can be proved to coincide with the ordinary labelled early asynchronous bisimilarity, on image-finite processes, exploiting the n-approximants of the labelled equivalences. We recall that the class of image-finite processes is the largest subset I of processes that is derivation closed and s.t. P ∈ I implies that, for all µ, the set {P | P µ =⇒ P }, quotiented by alpha conversion, is finite. In the remainder of the paper, we omit the adjectives 'early' and 'asynchronous' in all bisimilarities. Definition 3 (Bisimulation). A relation R on processes is a bisimulation if whenever P R Q and P µ -→ P , then one of these two clauses holds:

1) there is Q such that Q μ = ⇒ Q and P R Q ; 2) µ = a b and there is Q such that Q | a b = ⇒ Q and P R Q .
Moreover the converse holds too, on the transitions from Q. Bisimilarity, ≈, is the largest bisimulation.

Theorem 4 ([18]

). On image-finite processes, relations and ≈ coincide.

III. SEQUENTIALITY

In this section we study sequentiality. We first formalise it by means of a type system, and then we examine its impact on behavioural equivalence.

A. Type system

As mentioned in Section I, intuitively, sequentiality ensures us that at any time at most one interaction can occur in a system; i.e., there is a single computation thread. A process that holds the thread decides what the next interaction can be. It does so by offering a single particle (input or output) that controls the thread. The process may offer multiple particles, but only one of them may control the thread. The control on the thread attached to a particle is determined by the subject name of that particle. A given name may exercise the control on the thread either in output or in input; in the former case we say that the name is output-controlled, in the latter case the name is input-controlled. For instance, suppose that x, y, z are output-controlled and u, v are input-controlled. Then the following process correctly manages the thread and will indeed be typable in our type system:

P def = u. (x | y. x) | z. y | v
The initial particles in P are u, z, v; however only u controls the thread, as z is output-controlled and v is input-controlled. When the input at u is consumed, the new particles x, y are available, where x now controls the thread, as both names x, y are output-controlled. An external process that consumes the particle x will acquire the control over the thread. For instance, a process such as Q def = u | x. Q initially does not hold the thread; in the parallel composition P | Q, after the two interactions at u and x, the control on the thread will be acquired by Q :

P | Q -→-→ (y. x | z. y | v) | Q
Now Q will decide on the next interaction; for instance, it may offer an output at y or z, or an input at v. It may only offer one of these, though it may offer other particles that do not control the thread. Notation. In the remainder, x, y, z range over outputcontrolled names, u, v, w over input-controlled names; we recall that a, b, c range over the set of all names.

The name used is therefore an indication of its type. For instance, in (νx)P , x is output-controlled, and can be only alpha-converted using another output-controlled name.

The type system for sequentiality is presented in Figure 1. Judgements are of the form η s P , for η ∈ {0, 1}. A judgement 1 s P indicates that P owns the thread, i.e., P is active, and 0 s P otherwise, i.e., P is inactive.

We recall that we only present the additional typing constraints given by sequentiality, assuming the existence of a sorting under which all processes are well-typed (thus the fully-fledged typing judgements would be the form ∆; η s P , rather than η s P ).

Some remarks on the rules in Figure 1: a rule with a double conclusion is an abbreviation for more rules with the same premises but separate conclusions. The continuation of an input always owns control on the thread; the input itself may or may not have the control (rules I-ACT and I-INA). A τ -prefix is neutral w.r.t. the thread. The rule for parallel composition makes sure that the control on the thread is granted to only one of the components; in contrast, in the rule for sum, the control is maintained for both summands. Operators 0 and match cannot own the thread; this makes sure that the thread control is always exercised.

We present some behavioural properties that highlight the meaning of sequentiality. A reduction P τ -→ P is an interaction if it has been obtained from a communication between an input and an output (formally, its derivation in the LTS of [START_REF]On sequentiality and well-bracketing in the π-calculus[END_REF] uses rule ACOMM). In a sequential system, one may not find two disjoint interactions. Proposition 5. Whenever η s P , there exists no P 1 , P 2 , a such that P ≡ (ν a)(P 1 | P 2 ) with P 1 τ -→ P 1 and P 2 τ -→ P 2 , and both these transitions are interactions.

An inactive process may not perform interactions. Proposition 6. If 0 s P , then there is no P with P τ -→ P and this transition is an interaction.

An inactive process may however perform τ -reductions, notably to resolve internal choices. In other words such internal choices represent internal matters for a process, orthogonal with respect to the overall interaction thread. The possibility for inactive processes to accommodate internal choices will be important in our completeness proof. However, an inactive process may only perform a finite number of τ -reductions. A process P is divergent if it can perform an infinite sequence of reductions, i.e., there are P 1 , P 2 , . . . , with P -→ P 1 -→ P 2 . . . P n -→ . . .. Proposition 7. If 0 s P then P is not divergent.

In contrast, an active process may be divergent, through sequences of reductions containing infinitely many interactions.

Sequentiality imposes constraints on the interactions that a 'legal' (i.e., well-typed) context may undertake with a process. For the definition of barbed bisimulation and equivalence we must therefore define the meaning of observability. The following definition of type-allowed transitions shows what such 'legal' interactions can be.

Definition 8 (Type-allowed transitions). We write η s P µ -→ P if η s P , and P µ -→ P , and one of the following clauses holds:

1) η = 0 2) µ = τ 3) η = 1 and µ = u a for some u, a or µ = (ν a)x b for some a, x, b.

Clause [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] says that all interactions between an inactive process and the context are possible; this holds because the context is active and may therefore decide on the next interaction with the process. Clause (2) says that internal reductions may always be performed. Clause (3) says that the only visible actions observable in active processes are those carrying the thread; this holds because the observer is inactive, and it is therefore up to the process to decide on the next interaction.

We now examine how typing evolves under legal actions. We recall that x stands for an output-controlled name. 1) if µ = x a , then η = 1.

2) if µ = (ν a)x b , then η = 0.

3) otherwise η = η.

I-ACT Weak type-allowed transition are defined as expected, exploiting the invariance of typing under reductions: η s P µ = ⇒ P holds if there are P 0 , P 1 with P =⇒ P 0 , η s P 0 µ -→ P 1 and P 1 =⇒ P .

1 s P 1 s u( a). P I-INA 1 s P 0 s x( a). P, !x( a). P O-ACT 1 s x a O-INA 0 s u a RES η s P η s (νa)P NIL 0 s 0 PAR η 1 s P η 2 s Q η 1 + η 2 s P | Q η 1 + η 2 ≤ 1 SUM η s G 1 η s G 2 η s G 1 + G 2 TAU η s P η s τ . P MAT 0 s G 0 s [a = b]G

B. Behavioural equivalence

To tune Definition 2 of barbed bisimulation and equivalence to the setting of sequentiality, we have to specify the meaning of observables. An observable η s P ⇓ a holds if there are P and an output action µ such that η s P µ = ⇒ P and the subject of µ is a. Following Definition 1, in barbed equivalence, the legal contexts are the η/η static contexts. We write barbed equivalence at η as η . Thus P η Q holds if η s P, Q and

E[P ] . ≈ η E[Q],
for any η and any η /η static context E.

We are now ready to define the labelled bisimilarity to be used on sequential processes, which is our main proof technique for barbed equivalence. A typed process relation is a set of triplets (η, P, Q) with η s P, Q.

Definition 11 (Sequential Bisimulation). A typed process relation R is a sequential bisimulation if whenever (η, P, Q) ∈ R and [η; P ] µ -→ [η ; P ], then one of the two following clauses holds:

1) there is

Q such that Q μ = ⇒ Q and (η , P , Q ) ∈ R; 2) µ = a b and there is Q such that Q | a b = ⇒ Q with (η , P , Q ) ∈ R.
Moreover, the converse of (1) and (2) holds on the transitions from Q. Processes P and Q are sequentially bisimilar at η, written P ≈ η s Q, if (η, P, Q) ∈ R for some sequential bisimulation R.

In clause (2), Q | a b is well-typed, be a an input-or output-controlled name. Clauses (1) and ( 2) are the same as for ordinary bisimilarity ≈ (Definition 3); typing however prevents certain transitions to be considered as challenge transitions in the bisimulation game. Thus the resulting bisimilarity becomes coarser.

Ordinary bisimilarity is included in the sequential one (the inclusion is strict, see Section III-C).

Proposition 12. For η s P, Q, if P ≈ Q then also P ≈ η s Q. Theorem 13 (Soundness). If P ≈ η s Q, then P η Q. As usual, the proof of Theorem 13 relies on the preservation of ≈ η s under parallel composition, which requires some care in order to enforce sequentiality. This is ensured by typability. Theorem 13 allows us to use the labelled bisimilarity ≈ η s as a proof technique for typed barbed equivalence.

This proof technique is also complete, assuming only output-controlled names (i.e., the thread may only be exercised by output particles, not by the input ones).

Theorem 14 (Completeness on output-controlled names). For all image-finite processes P, Q that only use output-controlled names, and for all η, if P η Q then P ≈ η s Q. The completeness proof can be found in [START_REF]On sequentiality and well-bracketing in the π-calculus[END_REF]. While the overall structure of the proof is standard, the technical details are specific to sequentiality. As usual, we rely on a stratification of bisimilarity and approximants ≈ η,n s , and reason by contradiction to show that if η s P, Q and

P ≈ η,n s Q, then there is a η /η static context E such that E[P ] . ≈ η E[Q]. The case η = 0 (tested processes are inactive) is rather standard: the context E is of the form (ν x)([•] | z | z. R),
for some fresh z, and some "tester process" R. The barb at z allows us to detect when the tested process interacts with R.

The delicate case is when η = 1 (tested processes are active): the context must be inactive and hence cannot have an unguarded output at z. We use in this case a context of the form

E def = (ν x)([•] | G R + G).
Process G R is the tester process, and G is y∈S y( y ). z, defined for some fresh z and some set S containing fn(P ) ∪ fn(Q). G satisfies the following property: for any P 0 and for any x, if 1 s P 0 ⇓ x then 1 s P 0 | G ⇓ z . Thus, as soon as P 0 exhibits some barb, we have 1 s E[P 0 ] ⇓ z , and P 0 cannot interact with R without removing the barb at z, which allows us to reason as in the case η = 0.

The proof schema above does not apply if input-controlled names are allowed, intuitively because in this case the processes being tested may be active and perform an input (at an input-controlled name), thus maintaining the thread; both before and after the transition the testing context is passive and hence unable to signal, with appropriate barbs, which interaction occurred.

C. Examples

With respect to ordinary bisimilarity, in sequential bisimilarity (≈ η s ) fewer challenges are allowed. This may both mean that certain processes, otherwise distinguishable, become equal, and that certain equalities are simpler to prove because the state space of the processes to be examined is reduced. We present some equalities of the first kind (valid for ≈ η s only).

In Section III-C2, we also show a refinement of ≈ η s useful for reasoning about references.

1) Basic examples: In the type system, 0 is inactive -without the thread. We write 0 1 to abbreviate (νx)(x) (an active process without transitions).

Example 15. While a component of a system is active, other components cannot be observed. Thus, if the active component keeps the thread, the existence of other components is irrelevant. Indeed we have, for any R, Q inactive:

R | 0 1 ≈ 1 s R | (νx)(x | !x. x) ≈ 1 s Q | (νx)(x | !x. x) ≈ 1 s 0 1 Example 16.
An unguarded occurrence of an input at an input-controlled name becomes the only observation that can be made in a process. This yields the following equalities

u. P | x. Q ≈ 1 s u. (P | x. Q) u. P | v ≈ 1 s u. (P | v) for u = v
Example 17. Consider the process

P def = (νy , z )(!x. (z . z | y ) | !y. z ).
The output at z becomes observable if both an input at x and an input at y are consumed, so that the internal reduction at z can take place. However the input at x acquires the thread, preventing a further immediate input at y; similarly for the input at y. Indeed we have P ≈ 0 s x. 0 1 + y. 0 1 .

2) Examples with references:

We now consider a few examples involving references. For this, we use the standard encoding of references into Aπ, and we enhance the bisimilarity for sequentiality so to take references into account.

We use n, m, . . . to range over the entities stored in references (which can be names or values belonging to a firstorder data type like booleans and integers) and placeholders for them. Name is used to represent a reference.

In Aπ, a reference holding a value n is represented as an output particle n . A process that contains a reference should have, at any time, exactly one unguarded output at , meaning that at any time the reference has a unique value. We say that in this case is accessible. The read and write operations on are written as follows:

re (m). R def = (m). ( m | R) wr n . R def = (m ). ( n | R) for m / ∈ fn(R)
Thus a name used to encode a reference is input-controlled, as an action on a reference is represented by an input at -we use rather than u, v, . . . to stress the fact that names used to represent references obey constraints that go beyond input-control. Proof techniques for the representation of references in Aπ have been studied in [START_REF] Hirschkoff | On the representation of references in the pi-calculus[END_REF]. Adopting them requires enhancing our type system with information about references, which simply consists in declaring which names represent references. In the definition of barbed equivalence, the main constraint is that the tested context should make sure that all existing reference names are accessible. To reason about references, several definitions of labelled bisimilarity are presented in [START_REF] Hirschkoff | On the representation of references in the pi-calculus[END_REF], varying on the forms of constraints imposed on transitions. Here we only import the simplest such constraint: it forbids observations of input transitions P n -→ P at a reference name when is accessible in P (i.e., an unguarded output at occurs in P ). Such a constraint represents the fact that an observer may not pretend to own a reference when the reference is accessible in the process.

Formally, with the addition of references, judgements in the type system become of the form S; η s P , where S is a finite set of reference names, meaning that η s P holds and that S is the set of accessible reference names in P . The definition of type-allowed transitions, S; η s P µ -→ P , is the same as before (Definition 8) with the addition, in clause (3), of the constraint if µ is an input n at a reference name then ∈ S. ( * )

Finally the definition of sequential bisimilarity with references at (S, η), written ≈ S;η s is the same as that of sequential bisimilarity (Definition 11), just using S; η s P, Q and S; η s P µ -→ P in place of η s P, Q and η s P µ -→ P . It is straightforward to extend the soundness proof for sequential bisimilarity w.r.t. barbed equivalence (Theorem 13) to the case of sequential bisimilarity with references. Example 18. This example shows that reading or writing on a global reference is not subject to interferences from the outside, as these operations require the thread:

n | re (m). R ≈ ;1 s n | R{ n /m} n | wr m . R ≈ ;1 s m | R
Indeed, in each law, if P (resp. Q) is the process on the lefthand (resp. right-hand) side, then the relation {(( ; 1), P, Q)}∪ I is a sequential bisimulation, when taking the constraint ( * ) for references into account.

Example 19 (Fetch-and-add, swap). We consider fetch-andadd and swap operations, often found in operating systems. The first, written faa n (m) atomically increments by n the content of the reference , and returns the original value as m; the second, written sw n (m), atomically sets the content of to n and returns the original value as m:

faa n (m). R def = (m). ( m + n | R) sw n (m). R def = (m). ( n | R)
These operations may be mimicked by a combination of read and write operations (we take m / ∈ fn(R)):

faa2 n (m). R def = re (m). wr m + n . R = (m). ( m | (m ). ( m + n | R)) sw2 n (m). R def = re (m). wr n . R = (m). ( m | (m ). ( n | R))
For this mimicking to be correct, sequentiality is necessary.

To see this, consider the simple case when R def = c m . In the ordinary Aπ, processes sw n (m). R and sw2 n (m). R are distinguished, intuitively because the observer is capable of counting the two inputs and the two outputs at in sw2 n (m). R (against only one in sw n (m). R) and/or is capable of detecting the output m in sw2 n (m). R.

The processes are also distinguished with the proof techniques for references in [START_REF] Hirschkoff | On the representation of references in the pi-calculus[END_REF], intuitively because, after the initial input (m) (whereby the processes read the content of the reference), an observer may interact with the derivative of sw2 n (m). R and use its output m so to know the value that had been read. Such an observation is not possible with sw n (m). R.

In contrast, the two processes are equal if we take sequentiality into account. That is, we have: is a sequential bisimulation. The second law is treated similarly. In both cases, the relation exhibited is finite.

sw n (m). R ≈ ∅;1 s sw2 n (m).
For the third equality, one defines R as

∪ n (( ; 1), n | re (m ). R{ n /m}, n | R{ n, n /m, m })
Then {((∅; 1), re (m). re (m ). R, re (m). R{ m /m })} ∪ R ∪ I is a sequential bisimulation.

IV. WELL-BRACKETING

A. Type System

We now go beyond sequentiality, so to handle wellbracketing. In languages without control operators, this means that return-call interactions among terms follow a stack-based discipline.

Intuitively, a well-bracketed system is a sequential system offering services. When interrogated, a service, say A, acquires the thread and is supposed to return a final result (unless the computation diverges) thus releasing the thread. During its computation, A may however interrogate another service, say B, which, upon completion of its computation, will return the result to A. In a similar manner, the service B, during its computation, may call yet another service C, and will wait for the return from C before resuming its computation. B may also delegate to C the task of returning a result to A. In any case, the 'return' obligation may not be thrown away or duplicated.

The implementation of this policy requires continuation names. For instance, when calling B, process A transmits a fresh name, say p, that will be used by B (or other processes delegated by B) to return the result to A. Moreover, A waits for such a result, via an input at p. Therefore continuation names are linear [START_REF] Kobayashi | Linearity and the picalculus[END_REF] -they may only be used once -and input receptive [START_REF]The name discipline of uniform receptiveness[END_REF] -the input-end of the name must be made available as soon as the name is created; and they are output-controlled: they carry the thread in output.

In short, the 'well-bracketing' type system defined in this section refines the type discipline for sequentiality by adding linear-receptive names and enforcing a stack discipline on the usage of such names. Proof techniques for well-bracketing will be studied in Section IV-D.

Thus, with well-bracketing, we have three kinds of names: output-controlled names (ranged over by x, y, z, . . .) and inputcontrolled names (ranged over by u, v, w. . .), as in the previous section; and continuation names, ranged over by p, q, r. . .. As before, names a, b, c. . . range over the union of output-an input-controlled names.

Continuation names may only be sent at output-controlled names. Indeed, any output at an output-controlled name must carry exactly one continuation name. Without this constraint the type system for well-bracketing would be more complex, and it is unclear whether it would be useful in practice. By convention, we assume that, in a tuple of names transmitted over an output-controlled name, the last name is a continuation name. We write a, p for such a tuple of names.

The type system is presented in Figure 2. Judgements are of the form σ wb P where σ is a stack, namely a sequence of inputand outputtagged continuation names, in which the input and output tags alternate, always terminating with an output tag unless the sequence is empty:

σ ::= σ O | σ I σ O ::= p : o, σ I σ I ::= p : i, σ O | ∅
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, as for p in p : i, p : o, p : i, σ. We write p ∈ σ if name p appears in σ, and |σ| for the length of the sequence σ.

Intuitively, a stack expresses the expected usage of the free continuation names in a process. For instance, if p 1 : o, p 2 : i, p 3 : o, p 3 : i, p 4 : o wb P then p 1 , . . , p 4 are the free continuation names in P ; among these, p 1 will be used first, in an output (p 1 may be the subject or an object of the output); then p 2 will be used, in an input interaction with the environment. P possesses both the output p : o wb P p = q q : i, p : o wb q( a). P

WB-INP2

p : o wb P ∅ wb x( a, p). P, !x( a, p). P

σ wb P σ wb Q σ wb P | Q σ ∈ inter(σ; σ ) WB-TAU σ wb P σ wb τ . P |σ| ≤ 1 WB-SUM σ wb P σ wb Q σ wb P + Q |σ| ≤ 1 Fig. 2.
Type system for well-bracketing and the input capability on p 3 , and may use both capabilities by performing a reduction at p 3 ; or P may transmit the output capability and then use the input one; 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. The Subject Reduction Theorem 25 will formalise the behaviour concerning continuations names in stacks.

As simple examples of typing, we can derive p : o wb p a and p : o wb u(a). p a

In the latter typing, by rule WB-INP3, an input at an inputcontrolled name has the thread, and does not affect the stack because u is not a continuation name.

The same stack can be used to type a process that invokes a service at x before sending the result at p, as in p : o wb (νq)(x b, q | q(c). p c ) where q is a fresh continuation name created when calling x. To type the process without the restriction at q, the stack should mention the input and output capabilities for q: q : o, q : i, p : o wb x b, q | q(c). p c For another example, the process P 0 def = p(a). p a | q(b). q b can be typed using two stacks: we have both p : i, p : o, q : i, q : o wb P 0 and q : i, q : o, p : i, p : o wb P 0 . The choice of the stack depends on whether the call answered at p has been made before or after the call answered at q.

We comment on the rules of the type system. In WB-OUT1 and WB-OUT2 the obligation in the stack is fulfilled (the output capability on the only name in the stack is used in WB-OUT1 and transmitted in WB-OUT2). As explained above, the last name in the tuple transmitted at x is a continuation name, and the only one being transmitted (to enforce the stack discipline). In contrast, in WB-OUT3 an output at an inputcontrolled name does not own the thread and therefore may not carry continuation names. In WB-INP1 the input-tagged name on top of the stack is used. Rule WB-INP2 is the complement of WB-OUT2. In WB-INP3, an input at an input-controlled name maintains the thread. In all rules for input and τ prefixes, the stack in the premise of the rules may not contain inputtagged continuation names because their input capability must be unguarded (as they are receptive names). The same occurs in rule WB-SUM, following [START_REF]The name discipline of uniform receptiveness[END_REF] where choice on inputs at receptive names is disallowed (though the constraint could be relaxed). Matching is allowed on plain names, but not on continuation names; this is typical of type systems where the input and output capabilities on names are separate [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]; moreover, no continuation name may appear in the process underneath, to make sure that the obligations on continuation names are not eschewed. In WB-RES1 a continuation name is created, and then its output and input capabilities are inserted into the stack. In the rule, ξ, σ is a decomposition of the stack for νp P where σ is a stack beginning with an output tag; hence ξ is either empty or it is of the form σ , p : i, (i.e. ξ is an initial prefix of the stack, either empty or ending with an input tag).

Rule WB-RES2 is for continuation names that do not appear in the body of the restriction (this form of rule is common in type systems for linearity, to simplify the assertion of Subject Reduction). In rule WB-PAR, the typing stack is split to type the two process components P 1 and P 2 ; splitting of the typing is usual in type systems with linearity. Here, however, the split must respect the order of the names. That is, the stack in the conclusion should be an interleaving of the two stacks in the premises, as by the following definition.

Definition 21 (Interleaving). We write σ 1 ∈ inter(σ 2 ; σ 3 ) if (i) σ 1 is a stack, and (ii) σ 1 is an interleaving of σ 2 and σ 3 as by the following inductive rules: 1) ∅ ∈ inter(∅; ∅) 2) p : o, σ 1 ∈ inter(σ 2 ; p : o, σ 3 ) if σ 1 ∈ inter(σ 2 ; σ 3 ) 3) p : o, σ 1 ∈ inter(p : o, σ 2 ; σ 3 ) if σ 1 ∈ inter(σ 2 ; σ 3 ) 4) the same as ( 2) and (3) with p : i instead of p : o If a name appears both in σ 2 and in σ 3 with the same tag, then inter(σ 2 ; σ 3 ) may not contain any stack.

Being stack-ordered means that p. q | q. p cannot be typed.

Lemma 43. If R is a wb-bisimulation up-to static contexts and up-to deterministic reductions, then (σ, P, Q) ∈ R implies P ≈ σ wb Q. 1) Completeness: As in Section III, we prove completeness for processes that only use output-controlled names.

Theorem 44 (Completeness). For all image-finite, discreet and clean processes P, Q that only use output-controlled names, and for all σ, if P σ Q then P ≈ σ wb Q. As for Theorem 14, the crux of the proof is defining the discriminating static contexts. The additional difficulty is related to receptiveness of continuation names: we cannot use z. R or G R + T , as in Section III, when the tester process, R or G R , contains an input at a free continuation name.

Suppose σ wb P , for P discreet and clean. We decompose σ as ξ, p 1 : o, q 1 : i, . . . , p n-1 : o, q n-1 : i, p n : o for ξ = ∅ or ξ = q : i, and then define, for fresh q n and x i ,

E xi σ def = (ν p i , q i )([•] | i≤n p i ( y). x i y, q i ).
We have ξ, q n : o wb E xi σ [P ]. Intuitively, E xi σ forwards information from the p i 's (which are in σ) to the x i 's. Accordingly, the tester process can use names in x i (rather than in p i ), and can use them in input.

Let fn o (-) denote the set of free output-controlled names. We distinguish two cases. If ξ = ∅, then P is active. To follow the reasoning in the proof of Theorem 14, we work with E of the form

(ν x)(E xi σ | R + y∈S y( y , p). z p ),
for some set S ⊇ fn o (P ) ∪ fn o (Q) ∪ x i and fresh z. If ξ = q : i, then P is inactive. We reason with E of the form (ν x, q)(E xi σ | z q | z(q ). R). By typing, only the continuation name q received at z may appear free in R. Such q will be instantiated with q and then R will use it to test the input at q from the tested processes. (A restriction on q is needed, as the overall process has to be clean.)

In both cases, the resulting E is a q n : o/σ static context where q n is a fresh continuation name. More details on the proof can be found in [START_REF]On sequentiality and well-bracketing in the π-calculus[END_REF].

2) An Example: We explain how the techniques we have introduced allow us to reason about a well-known example, the well-bracketed state change (sometimes called 'awkward', or 'very awkward', example) [START_REF] Ahmed | State-dependent representation independence[END_REF], [START_REF] Dreyer | The impact of higher-order state and control effects on local relational reasoning[END_REF], [START_REF] Jaber | Syteci: automating contextual equivalence for higherorder programs with references[END_REF]. It is usually presented in ML thus: Function M 2 makes two calls to an external function y and returns 1. The other term, M 1 , between the two calls, modifies a local reference , which is then used to return the final result. Intuitively, equivalence between the two functions holds because: (i) the reference in M 1 represents a local state, not accessible from an external function; (ii) computation respects well-bracketing (e.g., the language does not have control operators like call/cc).

Below are the translations of M 1 and M 2 , following a standard encoding of functions and references in Aπ, and using the notations for references from Section III-C2:

[[M 1 ]] p def = (νx, )( 0 | Q) with Q def = p x | !x(y, p). wr 0 . (νq)(y q | q. wr 1 . (νr)(y r | r. re (n). p n )) [[M 2 ]] p def = (νx)(p x | !x(y, p). (νq)(y q | q. (νr)(y r | r. p 1 ))) [[M 1 ]] p has a unique transition, [[M 1 ]] p (νx)p x ------→ P 1 . Sim- ilarly, let P 2 be the unique derivative from [[M 2 ]] p . The equivalence between [[M 1 ]] p and [[M 2 ]] p follows immediately from P 1 ≈ ∅ wb P 2 .
To prove the latter, we exhibit a relation R containing the triple (∅, P 1 , P 2 ) and show that R is a wbbisimulation up-to deterministic reductions and static context. For an example of the importance of well-bracketing, R contains the triple

q 2 : i, p 2 : o, r 1 : i, p 1 : o, (ν )( 0 | Q | q 2 . wr 1 . (νr 2 )(y r 2 | r 2 . re (n). p 2 n )) | r 1 . re (n). p 1 n ), P 2 | q 2 . (νr 2 )(y r 2 | r 2 . p 2 1 ) | r 1 . p 1 1
Without the well-bracketing constraint, the first process in the triple could perform an input at r 1 , an internal transition, and finally an output p 1 0 . The second process cannot emit 0, which would allow us to distinguish P 1 and P 2 . With wellbracketing, since r 1 is not on top of the stack in the triple, the initial transition on r 1 is ruled out.

The details of the definition of R can be found in [START_REF]On sequentiality and well-bracketing in the π-calculus[END_REF]. In the same Appendix, we also discuss a simplified example, which exposes the main difficulties. The primary simplification consists in using linear functions. Some twisting in the ML terms is however necessary, as M 1 and M 2 become equivalenteven dropping well-bracketing -if they can be used at most once.

V. RELATED WORK AND CONCLUSIONS

Sequentiality is a form of linearity, hence our type system has similarity with, and borrow ideas from, systems with linear types, in languages for concurrency or functional languages, including types for managing locks as in [START_REF]A type system for lock-free processes[END_REF]. The type system in [START_REF] Levi | Controlling interference in ambients[END_REF] ensures one that terms of the Ambient calculus are single-threaded, a notion similar to the sequentiality for Aπ examined in this paper. The type system in [START_REF] Berger | Sequentiality and the picalculus[END_REF] has been designed so to make the encoding of PCF into the π-calculus fully abstract. The system therefore goes beyond sequentiality as described in our paper. For instance, the system presents a form of duality on types and ensures that computations are stateless, hence also deterministic. Indeed, the only behaviours inhabited by the types are those in the image of the PCF terms. Types ensure the uniqueness of the computation thread, and such a thread is carried by outputs (the thread cannot be carried by input processes, as in our system). The system [START_REF] Berger | Sequentiality and the picalculus[END_REF] has been further refined in [START_REF] Yoshida | Strong normalisation in the pi -calculus[END_REF], adding causality information and acyclicity constraints, so to ensure strong normalisation of well-typed processes. The issue of finding labelled bisimilarity characterisations of barbed equivalence or reduction-closed barbed equivalence is extensively discussed in [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]; see also [START_REF] Hennessy | Typed behavioural equivalences for processes in the presence of subtyping[END_REF] for an example involving types.

Type systems for linearity and receptiveness in the πcalculus have been introduced in [START_REF] Kobayashi | Linearity and the picalculus[END_REF], [START_REF] Igarashi | Type reconstruction for linear -calculus with I/O subtyping[END_REF], [START_REF]The name discipline of uniform receptiveness[END_REF]. The way we formulate well-bracketing (Definition 36) is inspired by 'well-bracketed strategies' in game semantics [START_REF] Hyland | On full abstraction for PCF: i, ii, and III[END_REF], [START_REF] Laird | Full abstraction for functional languages with control[END_REF], used in functional programming languages and extensions thereof (they have in turn inspired type systems for π-calculi with stack-like information and input/output alternation, e.g., [START_REF] Berger | Sequentiality and the picalculus[END_REF], [START_REF] Honda | Processes and games[END_REF]). The notion of well-bracketed control flow is studied in the field of secure compilation, for a wider class of languages. In works like [START_REF] Skorstengaard | Stktokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities[END_REF], [START_REF] Patrignani | On modular and fullyabstract compilation[END_REF], the technique of fully abstract compilation guarantees control flow correctness (and, in particular, well-bracketing) against low-level attacks.

Several methods have been proposed to establish contextual equivalence of sequential programs that include higher-order and stateful computation, including the above-mentioned game semantics, (step-indexed Kripke) logical relations [START_REF] Ahmed | State-dependent representation independence[END_REF], [START_REF] Dreyer | The impact of higher-order state and control effects on local relational reasoning[END_REF], dedicated forms of bisimulations designed on top of an operational semantics of the languages [START_REF] Koutavas | Small bisimulations for reasoning about higher-order imperative programs[END_REF], [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF], [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF], [START_REF] Madiot | Bisimulations up-to: Beyond first-order transition systems[END_REF], [START_REF] Biernacki | A complete normal-form bisimilarity for algebraic effects and handlers[END_REF]. Works like [START_REF] Jaber | Syteci: automating contextual equivalence for higherorder programs with references[END_REF] or algorithmic game semantics [START_REF] Murawski | Algorithmic games for full ground references[END_REF], aim at automatically establishing contextual equivalences, by relying on model-checking techniques.

The main goal of this paper was to tailor some of the most prominent proof techniques in the π-calculus -those based on labelled bisimilarity -to the sequentiality and wellbracketing disciplines. This is instrumental to the use of the π-calculus as a model of programming languages, as sequentiality and well-bracketing are often found in programming languages or subsets of them. We have shown the usefulness of our techniques on a number of examples, that have mainly to do with the representation of functions and store -none of the equalities in the examples is valid in the ordinary bisimilarity of the calculus.

In Section III-C we have combined our proof technique for sequentiality with techniques concerning the representation of references in π-calculus from [START_REF] Hirschkoff | On the representation of references in the pi-calculus[END_REF]. The resulting technique allows us in some cases to reason about programs with store without an explicit representation of the store (as usually required in the techniques in the literature, recalled above). This avoids universal quantifications on the possible values contained in the store, thus reducing the size of the relation to consider, sometimes making them finite. Further possibilities of reducing the size of relations may be possible by adapting the rich theory of the 'up-to techniques' for the ordinary π-calculus to our bisimilarities, as exemplified by the up-to technique considered in Definition 42 and applied in Section IV-D2.

Our treatment of sequentiality raises a few technical questions that deserve further investigation. We would like to see whether our proof of completeness (Theorem 14) could be extended to handle input-controlled names. Similarly, we do not know whether the result still holds if internal choice is disallowed in inactive processes. The usual encoding of an internal choice τ . P + τ . Q in terms of parallel composition as (νc) (c | c. P | c. Q), for some fresh c, is not applicable because the latter process is active (for instance, the encoding is not valid within a context testing active processes). Indeed, if the result still holds, the current proof might require some significant modifications. For similar reasons, it is unclear if and how our completeness proof could be tuned to handle reduction-closed variants of barbed equivalence [START_REF] Honda | On reduction-based process semantics[END_REF], [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF].

In the asynchronous π-calculus considered in this paper, an interaction involves only one prefixed process (the input). Therefore, in the type systems, this process always acquires the control on the thread after the interaction. In a synchronous setting, in contrast, an interaction involves also an output prefix. Hence the type systems could be richer, specifying, for each name, where the control on the thread goes after an interaction at that name. The representation of references in Section III-C, however, might have to be revisited as it relies on the asynchronous model.

We have studied proof techniques for sequentiality and wellbracketing in the π-calculus based on labelled bisimilarities. We would like to examine also the impact of the disciplines on algebraic theory and modal logics.

Definition 9 .

 9 We write [η; P ] µ -→ [η ; P ] when η s P µ -→ P and:

Fig. 1 .

 1 Fig. 1. The typing rules for sequentiality

R

  This is proved by showing that the relation∪ m {(( ; 1), n | R{ m /m}, m | wr n . R{ m /m}) ∪ I ∪ {((∅; 1), sw n (m). R, sw2 n (m). R)}is a sequential bisimulation. The equivalence between faa n (m). R and faa2 n (m). R is established using a similar relation. Example 20 (Optimised access). Two consecutive read and/or write operations can be transformed into an equivalent single operation. wr n . wr m . R ≈ ∅;1 s wr m . R wr n . re (m). R ≈ ∅;1 s wr n . R{ n /m} re (m). re (m ). R ≈ ∅;1 s re (m). R{ m /m } For the first equality, one shows that I ∪ {((∅; 1), wr n . wr m . R, wr m . R)} ∪ {(( ; 1), n | wr m . R, m | R)}

p

  : o wb P p : o wb u( a). P WB-NIL ∅ wb 0 WB-RES1 ξ, p : o, p : i, σ wb P ξ, σ wb (νp)P WB-RES2 σ wb P σ wb (νp)P p / ∈ σ WB-RES3 σ wb P σ wb (νa)P WB-MAT ∅ wb P ∅ wb [a = b]P WB-PAR

  fun y -> ( := 0; y() ; := 1; y() ; ! ) M 2 def = fun y -> (y() ; y() ; 1)

  resp. P i1 | . . . | P in ) where I = {i 1 , . . . , i n }. We write P { a /b} for the result of replacing name b with a in P in a capture-avoiding way. Contexts, C, are processes containing a single occurrence of a special constant, the hole (written [•]). The static contexts, ranged over by E, have the form ν a (P | [•]). In examples, for readability we sometimes use basic data values such as integers and booleans. The definition of structural congruence, written ≡, and of the strong and weak labelled transitions, written

µ

-→, = ⇒, and μ

Indeed, the left process would require p before q in the stack, whereas the right process needs the opposite.

In rule RES1, having the possibility to add names in the middle of the stack is mandatory to preserve typability after reduction. Consider for instance:

(νq)((νp)(b p | p. q) | q. p ) (νp)b p -----→ (νq)(p. q | q. p ) To type the derivative of the transition above, we have to use rule RES1 with ξ = p : i and σ = p : o.

Typability in the type system of Figure 2 implies typability in the type system for sequentiality. Indeed, when σ wb P , if the first name in σ is output-tagged then P is active, otherwise P is inactive. We write seq for the function that 'forgets' the well-bracketing information in a stack, therefore seq(σ) = 1 if σ = p : o, σ , for some p and σ , and seq(σ) = 0 otherwise. Proposition 22. If σ wb P then also seq(σ) s P .

In Definition 23, we extend type-allowed transitions to processes with continuation names. As previously, we must ensure that the process is typed, and that the transition is allowed by sequentiality (clauses (1) and (2) below). Clause (3) says that the first continuation name observed must be on top of the stack, and that the input or output capability on a continuation name may not be exercised by the environment when both capabilities are owned by the process. Definition 23. We write σ wb P µ -→ P when 1) σ wb P 2) seq(σ) s P µ -→ P and 3) if p ∈ fn(µ) and p ∈ σ, then either σ = p : o, σ or σ = p : i, σ for some σ ; moreover, if p ∈ σ , then p is not the subject of µ.

We exploit type-allowed transitions to define transitions with stacks, which make explicit the evolution of the stack.

) if µ = τ , then for σ = p : o, p : i, σ and p / ∈ fn(P ), we have σ = σ , otherwise σ = σ.

In cases (1), (4) (resp. ( 2)), we must have σ = p : o, σ (resp. p : i, σ ) by definition of type-allowed transitions. In clauses (1) and (2), the action is an input or an output at a continuation name that must be on top of σ, and is then removed. In clause (3), the action extrudes a continuation name, and then, following the stack discipline, the process waits for an answer on that name. In clause (4), emitting a free continuation name amounts to passing the output capability on that name to the environment. Dually, in clause [START_REF] Ancona | Behavioral types in programming languages[END_REF], receiving a continuation name imposes to use it in output. Finally, in clause [START_REF] Kobayashi | A partially deadlock-free typed process calculus[END_REF], a τ transition may come from an interaction at a continuation name, in which case σ is modified. It can also come from an interaction at a restricted name or from an internal choice; in such cases, σ is unchanged.

Theorem 25 (Subject Reduction). If σ wb P and [σ; P ] µ -→ [σ ; P ] then σ wb P .

If a process owns both the input and the output capability on a continuation name p, then the environment may not use p. Semantically, this is the same as having a restriction on p in the process. It is therefore safe, in the definition of barbed bisimulation and observability, to assume that all such restrictions are syntactically present, i.e., there is a single occurrence of any free continuation name. We call clean such processes.

Definition 26. A stack σ is clean if no name appears in σ both output-and input-tagged. A process P is clean if σ wb P for some clean σ.

On clean processes, typing is preserved by reduction.

Proposition 27. If σ wb P for σ clean, then P -→ P implies σ wb P .

Defining barbed bisimulation on clean processes, we can use the seq function above to recast observability in the wellbracketing system from that in the sequentiality system: thus, for σ clean, we have σ wb P ⇓ a (resp.

In the definition of barbed equivalence, the contexts testing the processes must be clean. Writing σ for barbed equivalence at σ, we have P σ Q if σ wb P, Q, and for any clean σ and any σ /σ static context E, it holds that E

(note that σ itself need not be clean).

B. Discreet Processes

In this section we put forward the subclass of discreet processes, in which all continuation names that are exported must be private, and show how to transform any process into a discreet one. Then, on discreet processes:

(1) we express a behavioural property that formalises the stack-like discipline on the usage of continuation names; (2) we develop proof techniques, in form of labelled bisimilarities, to reason about the behaviour of well-typed processes. (Concerning (2), while the technical details are quite different, we follow the approach of proof techniques for receptive names in [START_REF]The name discipline of uniform receptiveness[END_REF], where the techniques are first defined on processes where only fresh names may be sent.) Definition 28 (Discreet processes). A process P is discreet if any free continuation name p ∈ fn(P ) may not appear in the object of an output, and, in any sub-process x( a, q). Q, the same holds for q in Q. The definition is extended to contexts, yielding discreet contexts.

If E and P are discreet, then so is E[P ]. We can transform all well-typed processes into discreet processes using the law in Lemma 29 below. The law transforms the output of a global continuation name p into the output of a local name q. In general, all outputs of continuation names in a process P are local, as a global output corresponds to P delegating a stacklike obligation to another process. In other words, in general the transformation of a non-discreet process into a discreet one will modify only a few outputs of the initial process. The law in Lemma 29 is valid for barbed congruence, not just barbed equivalence, and may therefore be applied to any component of a given process.

Lemma 29. x a, p ∼ = p:o (νq)(x a, q | q( b). p b ).

Thus, in the definition of barbed equivalence (and congruence) it is sufficient to consider discreet contexts.

A discreet process may only export private continuation names. Dually, the process may only receive fresh continuation names from a discreet context. We call discreet the transitions that satisfy this property.

Definition 30 (Discreet transitions). A typed transition σ wb P µ -→ P is discreet if any continuation name in the object of µ is not free in σ (and hence also in P ).

Lemma 31. If P is discreet, and σ wb P µ -→ P is discreet, then P is discreet. If, moreover, P is clean, then so is P .

C. The Well-bracketing property on traces

Following game semantics [START_REF] Hyland | On full abstraction for PCF: i, ii, and III[END_REF], we formalise wellbracketing, that is, the stack-like behaviour of continuation names for well-typed processes, using traces of actions. In this section, all processes are discreet and clean. A trace for such a process is obtained from a sequence of discreet transitions emanating from the process, with the expected freshness conditions to avoid ambiguity among names.

Definition 32 (Trace). A sequence of actions µ 1 , . . . , µ n is a trace for a (discreet and clean) process P 0 and a stack σ 0 if there are σ 1 , . . . , σ n , P 1 , . . . , P n such that for all 0 ≤ j < n we have [σ j ; P j ] µj+1 ---→ [σ j+1 ; P j+1 ], where the transition is discreet, and moreover all continuation names appearing as object in µ j+1 are fresh (i.e., the names may not appear in any µ i for i ≤ j).

The notion of discreet transition already imposes that continuation names in object position do not appear free in the process. The final condition in Definition 32 on continuation names ensures us that for actions like (νp)x a, p , name p is fresh, and that after an action p a (thus the only allowed interaction at p has been played), name p cannot be reintroduced, e.g., in an action x a, p . We simply say that µ 1 , . . . , µ n is a trace, or is a trace for P , when the stack or the process are clear from the context.

The well-bracketing property is best described with the notion of questions and answers.

Definition 33. For a trace µ 1 , . . . , µ n , we set µ i µ j if i < j and:

1) either µ i = (ν c, p)a b, p and µ j = p a , 2) or µ i = a b, p and µ j = (ν c)p a .

Actions µ i (with a continuation name in object position) are called questions, while actions µ j (with a continuation name in subject position) are called answers.

A discreet transition is either an internal transition, or a question, or an answer. A question mentioning a continuation name p is matched by an answer at p. When questions and answers are seen as delimiters ('[ p ','] p ', different for each continuation name), a well-bracketed trace is a substring of a Dyck word.

Remark 34. For a discreet transition [σ; P ] µ -→ [σ ; P ], the value |σ | -|σ| is 1 for a question, 0 for an internal action, and -1 for an answer.

Lemma 35 (Uniqueness). Given a trace µ 1 , . . . , µ n , if µ i µ j and µ i µ j , then we have (i = i iff j = j ).

Definition 36 (Well-bracketing). A trace µ 1 , . . . , µ n is wellbracketed if for all i < j, if µ i is a question and µ j is an answer with µ i µ k and µ k µ j for all i < k < j, then µ i µ j .

To prove that all traces are well-bracketed, we need the following property relating questions and answers to stacks. Lemma 37. Let µ 1 , . . . , µ n be a trace, and σ 0 , . . . , σ n be the corresponding stacks, as in Definition 32. Suppose σ 0 = σ n , and for all i,

Proposition 38. Any trace (as by Definition 32) is wellbracketed.

D. Bisimulation and Full Abstraction

As in Section III, a wb-typed relation on processes is a set of triplets (σ, P, Q) with σ wb P, Q.

Definition 39 (WB-Bisimulation). A wb-typed relation R on discreet processes is a wb-bisimulation if whenever (σ, P, Q) ∈ R and [σ; P ] µ -→ [σ ; P ] is discreet, then one of the three following clauses holds:

a, p and for some fresh q, there is

(σ , P , Q ) ∈ R, and symmetrically for the transitions from Q.

Processes P and Q are wb-bisimilar at σ, noted P ≈ σ wb Q, if (σ, P, Q) ∈ R for some wb-bisimulation R.

Compared to Definition 11, the clause for input actions is here split into two clauses. In clause (2), we apply Lemma 29 to obtain a discreet process.

WB-bisimulation is sound with respect to barbed equivalence for all discreet processes. The main result concerns preservation by parallel composition:

Lemma 40 (Parallel composition). If P ≈ σ wb Q, then for any discreet process R and stacks σ , σ such that σ wb R and σ ∈ inter(σ; σ ), we have

Note that even if P, R are clean, P | R needs not be so.

Theorem 41 (Soundness). ≈ σ wb ⊆ σ . To prove soundness, we show that ≈ σ wb is preserved by all discreet static contexts. By Lemma 29, we can then replace any non-discreet context with a discreet one.

We further refine the coinductive technique given by ≈ σ wb by introducing some up-to techniques, which make it possible to work with smaller relations. We write P -→ d P when the reduction is deterministic, meaning that whenever P µ -→ P , then µ = τ and P ≡ P . Similarly, we write P = ⇒ d P if all reduction steps are deterministic. Moreover, for a relation R, we write (σ, P, Q) ∈ = ⇒ d R C when there exists a stack σ , a σ/σ context E, and processes P , Q such that Q ≡ E[Q ], P = ⇒ d E[P ] and (σ , P , Q ) ∈ R.

Definition 42 (Up-to static contexts and up-to deterministic reductions). A wb-typed relation R on discreet processes is a wb-bisimulation up-to static contexts and up-to deterministic reductions if whenever (σ, P, Q) ∈ R, for any discreet transition [σ; P ] µ -→ [σ ; P ], one of the following clauses holds:

1) there is Q with Q μ = ⇒ Q and (σ , P , Q ) ∈ = ⇒ d R C , 2) µ = x a, p and for some fresh q, there is Q with Q | (νq)(x a, q | q. p) = ⇒ Q and (σ , P , Q ) ∈ = ⇒ d R C , 3) µ = u a and, there is

and symmetrically for the transitions from Q.