Giuseppe Castagna

Mariangiola Dezani-Ciancaglini

Elena Giachino

Luca Padovani

Foundation of Session Types

We present a streamlined theory of session types based on a simple yet general and expressive formalism whose main features are semantically characterized and where each design choice is semantically justified. We formally define the semantics of session types and use it to define the subsessioning relation. We give a coinductive characterization of subsessioning and describe algorithms to decide all the key relations defined in the article. We show that all monomorphic dyadic session types proposed in the literature are particular cases of our session types.

Introduction

Sessions are a common and widespread mechanism of interaction in distributed architectures. Two processes willing to interact establish a connection on a shared public channel. In this connection they agree on some private channel on which to have a conversation, dubbed session. The conversation follows a given protocol which describes the kind and order of the messages exchanged on the private channel. In general, a protocol does not specify a unique sequence of interactions. At any point of the interaction the rest of the conversation for a process may depend upon the kind of messages received by the process on the private channel and/or the internal state of the process. When the decision is exclusively based on the received messages one speaks of an external choice. When the decision is taken autonomously by the process one speaks of an internal choice. The messages exchanged during a session may be synchronization signals, basic values (e.g., integers, booleans, strings), names of public channels (those used to start sessions), or even names of private channels of already started sessions. In the last case one speaks of delegation since by sending to some other process the private channel of a session, the process delegates the receiver to continue that session.

In summary, session-based interaction is obtained from two ingredients, each ingredient being formed by two different components. The first ingredient is communication and takes place on two different kinds of channels, public channels used to establish a connection, and a private channel created at the connection of the former and on which messages of different kinds are exchanged according to a given protocol. The second ingredient is control, and it is implemented by two different kinds of choices, internal choices and external ones.

Static descriptions of the behavior of sessions (i.e., their protocol) should permit the detection of communication mismatches and session deadlocks, ensuring successful termination of every session. Types are a good candidate for such a description, except that typical type systems for process algebrae are unfit to type the private channels on which sessions take place, since these channels can carry messages of different types. To obviate this limitation Honda et al. introduced session types [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF] that describe the sequences of messages exchanged on a private session channel and their possible branching based on labels. To that end they enrich the language of types and of processes with specialized signals for connections, for delegation, and signals carrying labels that drive choices in combination with label-based branching primitives. Since then, several variants of session types have been put forward (see Section 3). They vary according to the programming language they target, the type containment relations and the specific features they aim to capture. As Honda et al., they rely on label-based primitives that tie them to the particular problem they tackle and may hinder their adoption in general purpose languages.

In this work we present a basic and unified foundation of session types that aims at being as much language independent as possible. To achieve language independence, we design our types around the standard π-calculus: session connections, interactions, and delegations will be imagined as instances of π-calculus communications. We suppose branching as being implemented by classic process algebra internal and external choices [START_REF] De Nicola | CCS without τ 's[END_REF], with just a single modification: we allow the branch of an external choice to be selected according to the type of the message being communicated, as opposed to the channel on which communication occurs. This modification fits nicely the session-based communication model, where messages are exchanged over a unique, private channel.

Our approach has many positive upshots. First, all monomorphic, dyadic session types proposed in the literature are particular instances of the session types discussed here. Second, having dissociated control from a particular linguistic construct, that is labeldriven branching, we can more easily type the native branching constructs of a language we want to endow with session types, thus avoiding clumsy language extensions. As an aside, the language independence is further increased by the fact that all our definitions are semantic-based, rather than syntax-oriented. Third, we enhance compositionality of branching constructs because the result of the combination of different branches is automatically computed at type level, without the need of introducing new labels or of renaming existing ones to avoid clashes on shared labels. Last but not least, replacing labels with values and types increases expressiveness: values are first class (so they can result from computations and communicated on channels) and types enable the definition of finer grained disciplines for branch selection.

The rest of the paper is organized as follows. Section 2 defines syntax and set-theoretic semantics of our session types. The subtyping and subsessioning relations that follow arise as natural consequences of our semantic-based framework. We provide a coinductive characterization of subsessioning that sheds light on the properties of subsessioning and finally we describe algorithms to decide all key relations defined in the article. Section 3 provides a more technical discussion about how our approach subsumes and improves existing session types proposals. Furthermore, it presents a π-calculus and an object-oriented calculus along with corresponding type systems guaranteeing a suitably defined progress property [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF] 2009/1/21 in each case. Section 4 summarizes the contributions of our work, draws connections with some of the most closely related papers, and sketches future directions of research.

Session types 2.1 Type syntax

As said in the introduction we have two kinds of channels: public ones that are used to connect and establish a private channel for the conversation, and these private ones. At type level this distinction corresponds to two different syntactic categories. Public channels are associated with a session type of the form begin.η. This type classifies channels ready to initiate a conversation on some private channel that will follow the description η. Thus, private channels are classified by session descriptors, ranged over by η. Session descriptors and types are defined by the grammar:

(types)

t ::= • • • | begin.η | ¬t | t ∧ t | t ∨ t | v (descriptors) η ::= end | α.η | η ⊕ η | η + η (actions) α ::= !t | ?t | !χ | ?χ (sieves) χ ::= η | ¬χ | χ ∧ χ | χ ∨ χ
Participants of a session use their (private) session channel either to exchange values (of some type) or to delegate other session channels (of some descriptor). In descriptors we use ?t and !t to denote that (the process using) the channel will respectively wait for and send some value of type t, and use ?η and !η (actually, ?χ and !χ, see later on) to denote that (the process that uses) the channel will respectively wait for (i.e., catch) and send (i.e., delegate) some channel which already started a conversation and will continue it according to the behavior described by the session descriptor η. In particular, a descriptor α.η states that (the process using) the channel will perform one of the communication actions α described above and then will behave according to η; a descriptor end states that the session on the channel has successfully ended; a descriptor η1 ⊕ η2 states that (the process that uses) the channel will internally choose to behave according to either η1 or η2; a descriptor η1 + η2 states that (the process that uses) the channel gives the communicating partner the choice to behave according to either η1 or η2. In what follows we adopt the convention that the prefix operator has precedence over the choice operators and we will use parentheses to enforce precedence. For instance, (!t.η) + end and !t.η + end denote the same session descriptor, which is different from !t.(η + end). Types t are inherited from the host language (this is stressed in the grammar above by the ellipsis in the production for types), to which we add (unless they are already provided by the host) singleton types (denoted by a value v, the only one they contain), Boolean combinators (i.e., ∨, ∧, and ¬), and session types of the form begin.η which classify yet-to-be-used public channels whose conversation follows the descriptor η. The interest of session types is that they can be used to type higherorder communications in which the names of public channels are communicated over other channels; session types will also extend the type system of the host language which can thus use names of public channels as first class values.

The importance of Boolean combinators for types is shown by the following example where we assume Int be a subtype of Real: ?Real.!Int.end + ?Int.!Bool.end

The session descriptor above declares that if a process (that uses a channel with that behavior) receives a real number, then it will answer by sending an integer, while if it receives an integer it will answer by sending a Boolean. A partner process establishing a conversation on such a channel knows that if it sends a real that is not an integer, then it should be ready to receive an integer while if it sends an integer, then it must be ready to receive an integer or a Boolean value (notice how the type of the message drives the selection of the external choice). That is, its conversation will be represented by the following descriptor (t \ s stands for t ∧ ¬s):

!(Real \ Int).?Int.end + !Int.?(Bool ∨ Int).end [START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF] We see that Boolean combinators immediately arise when describing the behavior of an interacting process. They are also useful when considering equivalences. For instance, [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF] is intuitively equivalent to ?(Real \ Int).!Int.end + ?Int.!(Bool ∨ Int).end

The crucial role of Boolean combinators can be further shown by slightly modifying [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF] so that it performs only input actions: ?Real.?Int.end + ?Int.?Bool.end [START_REF] Boreale | Sessions and pipelines for structured service programming[END_REF] In this case the descriptor declares that after receiving an integer it will either wait for another integer or for a Boolean value. If an interacting process sends an integer, then in order to be sure that the conversation will not be stuck it must next send a value that is both an integer and a Boolean. Since there is no such a value, the only way to successfully interact with ( 4) is to make sure that interacting processes will only send reals that are not integers: !(Real \ Int).!Int.end. In conclusion, the only way to describe the sessions that can successfully interact with ( 4) is to use negation (for the sake of completeness note that ( 4) is equivalent to ?(Real \ Int).?Int.end+?Int.?(Bool ∧ Int).end which is equivalent to ?(Real \ Int).?Int.end since the right summand of the previous choice can never successfully complete a conversation). A similar discussion can be done for delegation, that is, when actions are over session descriptors, rather than types. This is why we added Boolean combinations of session descriptors too (we dub them sieves) and actions have the form ?χ and !χ rather than ?η and !η.

We want both types and session descriptors to be recursively definable. This is important for types since it allows us to represent recursive data structures (e.g., DTDs) while for session descriptors it allows us to represent services that provide an unbounded number of interactions such as (the service whose behavior is the solution of the equation) η = end + ?Int.η which describes a session that accepts as many integers as wished by the interacting process. In order to support recursive terms, we resort to a technique already used in [START_REF] Frisch | Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types[END_REF][START_REF] Castagna | A theory of contracts for web services[END_REF] where instead of introducing an explicit finite syntax for recursive terms, we directly work with possibly infinite regular term trees that satisfy some contractivity conditions; these conditions ensure that terms are semantically meaningful. DEFINITION 2.1 (Types). The types of our system are the possibly infinite regular trees coinductively generated by the productions in the grammar at the beginning of this section that satisfy the following conditions:

1. on every infinite branch of a type there are infinitely many occurrences of "begin"; 2. on every infinite branch of a session descriptor there are infinitely many occurrences of "." (the prefix constructor); 3. for every subterm of the form α.η, the tree α.η is not a subtree of α.

The first two conditions are contractivity restrictions that rule out meaningless terms such as (the solutions of the equations) t = t ∨ t or η = η ⊕ η; technically they say that the binary relation defined by t1 ∨ t2 ti, t1 ∧ t2 ti, ¬t t, χ1 ∨ χ2 χi, χ1 ∧ χ2 χi, ¬χ χ, η1+η2 ηi, η1⊕η2 ηi is Noetherian (that is, strongly normalizing), which gives an induction principle on terms that we will use in our proofs without any further explicit reference to the relation . The third condition states that recursion cannot escape prefixes and thus it rules out terms such as η = ?η.end; this restriction generalizes the typing technique used in all works on (recursive) session types that forbids delegation of a channel over itself [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Yoshida | Language primitives and type disciplines for structured communication-based programming revisited[END_REF] (strictly speaking we disallow types that in the cited works are not inhabited by any program) while, technically, it allows us to stratify the definition of the subtyping and subsessioning relations, stratification we use in the proof of Theorem 2.6.

We do not specify any particular property for the types of the host language. If the host language has some type constructors (e.g., products, arrows, etc.) the first contractivity condition can be relaxed to requiring that on every infinite branch there are infinitely many occurrences of type constructors. The only condition that we impose on the host language is on values which must satisfy the following strong disjunction property for unions:

v : t1 ∨ t2 ⇐⇒ v : t1 or v : t2 (5)
This condition may be restrictive only in the case that the host language already provides a union type combinator since, otherwise, it can be easily enforced by requiring that every session channel is associated with exactly one (most specific, because of subtyping) session type. Henceforward, we will use t to range over types, θ and η to range over session descriptors, χ to range over sieves, ψ to range over all of them, and often omit the word "session" when speaking of session descriptors. We reserve v for values, whose definition and typing is left unspecified: we assume as understood that values for a session type begin.η are channels explicitly associated with or tagged by that type (or, because of subtyping, by a begin.η subtype of begin.η: more about that later on).

We do not include in our session descriptors a construct for parallel composition (as opposed to [START_REF] Igarashi | A generic type system for the picalculus[END_REF][START_REF] Caires | Conversation Types[END_REF], for example). Since we assume an interleaving semantics of parallel composition, having two different choices is enough for faithfully describing possibly concurrent actions by means of well-known expansion laws (see [START_REF] De Nicola | CCS without τ 's[END_REF] for an example).

The intuitive semantics of session descriptors we outlined above is formalized in the following section.

Semantics of types and descriptors

The semantics of both session descriptors and types-and more generally most of the constructions of this work-crucially relies on the notion of duality. In this section we first informally define duality to outline a denotational semantics for types and descriptors, then we give the formal definition of duality in terms of a labeled transition system for descriptors.

Set-theoretic interpretations

In the previous section we argued that a complete set of Boolean combinators must be used if we want to describe the set of partners that safely interact with a given descriptor. Since we want the semantics of Boolean combinators to be intuitive and easy to understand we base their definition on a set-theoretic interpretation. In particular, we interpret every type constructor as the set of its values and the Boolean combinators as the corresponding set-theoretic operations. In other terms, we seek for an interpretation of types

. such that t = {v | v : t} and that t ∧ s = t ∩ s , t ∨ s = t ∪ s , and ¬t = V \ t (where V denotes the set of all values). The same interpretation can then be used to define the subtyping relation (denoted by "<:") as follows:

t <: s def ⇐⇒ t ⊆ s
The technical machinery to define an interpretation with such properties and solve the problems its definition raises (e.g., the circularity between the subtyping relation and the typing of values) already exists and can be found in the work on Semantic Subtyping [START_REF] Frisch | Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types[END_REF]: we take it for granted and no longer bother about it if not for session types that are dealt with in Section 2.3. This interpretation of types justifies the use we do henceforward of the notation v ∈ t to denote that v has type t.

The next problem is to give a set-theoretic interpretation to session descriptors, as we have Boolean combinations on them too. This interpretation is not required to be precise or mathematically meaningful but only to ensure that conversations do not get stuck. To this aim, rather than giving the set of values (or whatever they would be, since session descriptors classify just "chunks" of conversation) contained in a descriptor, it suffices to characterize all the possible behaviors common to all channels that implement a given session. In other terms, the semantics of a session descriptor can be characterized by the set of partners with whom the interaction will never get stuck (a sort of realizability semantics). This is captured by the notion of duality: two session descriptors η and θ are dual if any conversation between two channels which follow respectively the prescriptions of η and θ will never get stuck. So, for instance, the descriptor (1) in the previous section is dual to the descriptor [START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF]. But !Int.?(Bool ∨ Int).end is dual to (1), too.

Note also that some session descriptors have no dual, for example ?(Bool∧Int).end, since no process can send a value that is both a Boolean and an integer: the intersection is empty. 1 Such descriptors constitute a pathological case, since no conversation can take place on channels conforming to them. Thus we will focus our attention on descriptors for which at least one dual exists, and that we dub viable descriptors. We write η θ if η and θ are dual (duality is a symmetric relation). Then, we can define the interpretation of a descriptor as the set of its duals: η = {θ | η θ}; extend it settheoretically to sieves: χ∧χ = χ ∩ χ , χ∨χ = χ ∪ χ , ¬χ = S \ χ (where S denotes the set of all viable descriptors); and use it to semantically define the subsieving (and subsessioning) relation (denoted by "≤"):

χ ≤ χ def ⇐⇒ χ ⊆ χ (6)
Duality plays a central role also in defining the semantics of types. We said that the semantics of a type constructor is the set of its values. Hence we have to define the values of the type constructor begin.η. As suggested in Section 2.1, we can take as a value of a session type a public channel tagged by that type or by a subtype. Therefore to define values we need to determine when a session type is subtype of another, that is, when we can safely use a channel of some session type where a channel of a different (larger) type is expected. The key is to understand how a public session channel is "used". We make the assumption-matched by everyday practice-that there is unique way to consume a public channel c of type begin.η, by invoking the service associated with c and starting a conversation that conforms to the protocol described by η. Thus it is safe to replace c with a different channel d of a smaller type begin.η only if the conversation, which follows the protocol described by η and which was originally intended to occur with the service associated with c, works seamlessly with the service associated with d. This happens if at each step of the conversation the service associated with d is willing to receive at least all the messages accepted by c and never sends any message that c would not send. Roughly speaking, the service associated with d is "more tolerant" than the one associated with c. Of course, there are fewer services that, as d, support a η conversation, since they must be able to satisfy more demanding clients. Therefore, passing from begin.η to begin.η corresponds to restricting the set of possible services one can safely use, that is to say, reducing the sets of possible duals. So the intuition-that we will formalize in Section 2.3 by equation [START_REF] De Nicola | Testing equivalences for processes[END_REF]-is that begin.η <: begin.η if and only if η has fewer duals than η, that is by [START_REF] Capecchi | Amalgamating Sessions and Methods in Object Oriented Languages with Generics[END_REF], η ≤ η. For instance we have that ?Int.end ≤ ?Real.end since every descriptor that is dual of ?Int.end is also dual of ?Real.end. Similarly begin.?Int.end <: begin.?Real.end since if a process that uses a channel of type begin.?Real.end is well typed, then the process obtained by replacing this channel for a different one of type begin.?Int.end is well typed as well: it will receive an integer number in a place where it expects a real number.

Since we want our types to satisfy the strong disjunction property [START_REF] Caires | Conversation Types[END_REF], then a public channel c must be tagged by types of the form begin.η (and not, say, begin.η ∨ begin.η ), which yields the following interpretation for session types: begin.η

= {c t | t <: begin.η} = {c begin.η | η ≤ η}, that is begin.η = {c begin.η | ∀θ, θ η ⇒ θ η} (7)
The next step is to formally define the duality relation for which we have to characterize the observables of the session descriptors.

Semantics of session descriptors

The formal semantics of a descriptor can be given by resorting to the labeled transition system (LTS) defined by the rules

(TR1) end -→ end (TR2) η ⊕ η -→ η (TR3) η -→ η η + η -→ η + η (TR4) η µ -→ η η + η µ -→ η (TR5) η !v -→ η η + η -→ η (TR6) η !η -→ η η + η -→ η (TR7) v ∈ t ?t.η ?v -→ η (TR8) v ∈ t !t.η !v -→ η (TR9) η ∈ χ ?χ.η ?η -→ η (TR10) η ∈ χ !χ.η !η -→ η
plus the symmetric of rules (TR2-TR6). In the rules µ ranges over actions of the form !v, or ?v, or !η, or ?η, or .

Rules (TR1-TR4) are straightforward: end emits a "tick" (TR1); an internal choice silently decides the behavior it will successively follow (TR2); an external choice either performs an internal silent move (TR3) or it emits a signal µ that it offers as a possible choice to the interacting partner (TR4). Note that internal moves in one branch of an external choice do not preempt the behavior of the other branch. This is typical of process languages with two distinct choice operators, such as CCS without τ 's [START_REF] De Nicola | CCS without τ 's[END_REF].

The remaining rules are somewhat less common . Rules (TR7-TR8) state that the synchronization is performed on single values (strictly speaking, on singleton types) rather than on generic types. This is closer to what happens in practice, since !t.η indicates that the descriptor is ready to emit some value of type t (TR8), while ?t.η indicates that the descriptor is ready to accept any value of type t (TR7). While this approach is reminiscent of the so-called early semantics in process algebras [START_REF] Milner | Modal logics for mobile processes[END_REF] (but note that here it is applied at type level rather than at process level), there is a technical reason to use values rather than types, which we explain after defining the subsessioning relation.

Rules (TR9-TR10) follow the same idea as (TR7-TR8), and state that actions on descriptors emit a more precise information than what they declare. To understand this point we need to give some details. First note that a session descriptor η, despite it is usually called "session type" in the literature, is not a "real" type since it does not type any value. Session descriptors do not classify values but, rather, they keep track of the residual conversation that is allowed on a given session channel (whose "real" type is of the form begin.η). Therefore we cannot directly apply the same technique as for rules (TR7-TR8) since there does not exist any value for session descriptors. To mimic the behavior of rules (TR7-TR8) we resort to the informal semantics we described in Section 2.2.1 where a type is interpreted as the set of its values and a descriptor-actually, a sieve-as the set of its duals: therefore, as an action on a type emits the same action on its values, so an action on a sieve emits the same action on its duals, where we use η ∈ χ to denote that η ∈ χ . 2Rules (TR5-TR6) state that outputs are irrevocable. This is a characteristic peculiar to our system and is reminiscent of Castellani and Hennessy's treatment of external choices in the asynchronous CCS [START_REF] Castellani | Testing theories for asynchronous languages[END_REF]. Roughly speaking, imagine a process offering two different outputs in an external choice. Then we can think of two possible implementations for such a choice. In one case the choice is an abstraction for a simple handshaking protocol that the communicating processes engage in order to decide which value is exchanged. This implementation does not fit very well a distributed scenario where processes are loosely coupled and communication latency may be important. In the second-and in our opinion closer to practice-case, the sender process autonomously decides which value to send. Rules (TR5-TR6) state that the decision is irrevocable in the sense that the sender cannot revoke its output and try with the other one. This behavior is obtained by rules (TR5-TR6) by assimilating an external choice over output actions to an internal choice in which the process silently decides to send some particular value. In this respect the symmetry of input and output actions in rules (TR7-TR8)-but the same holds for (TR9-TR10) as well-may be misleading: we implicitly assumed that when a process waits for a value of type t it is ready to accept any value of type t (the choice of the particular value is left to the sender) while when a process sends a value of type t, it internally decides a particular value of that type. We will break this symmetry in the formal notion of duality (Definition 2.5) to be defined next.

Duality

The discussion on the labeled transition system suggests that two dual descriptors can either agree on termination (so both emit ) or one of the two descriptors autonomously chooses to send an output that the other descriptor must be ready to receive. In order to formalize the notion of duality it is then handy to characterize outputs (when an output action may happen) and inputs (when an input action must happen). As usual we write =⇒ for the reflexive and transitive closure of -→; we write µ =⇒ for =⇒ µ -→ =⇒; we write η µ -→ if there exists η such that η µ -→ η , and similarly for µ =⇒; we write η -→ if there exists no η such that η -→ η . DEFINITION 2.2 (May and Must Actions). We say that η may output µ, written η ↓ µ, if there exists η such that η =⇒ η -→ and η µ -→ and µ is either !v, or !η, or . We say that η must input µ, written η ⇓ µ, if η =⇒ η -→ implies η µ -→ and µ is either ?v, or ?η, or . As usual we write η ↓ µ if not η ↓ µ and η ⇓ µ if not η ⇓ µ.

Intuitively η ↓ µ states that for a particular internal choice η will offer an output µ as an option, while η ⇓ µ states that the input µ will be offered whatever internal choice η will do. For example !Int.end ⊕ end ↓ !3 and !Int.end ⊕ end ↓ ; on the other hand we have !Int.end + end ↓ , since !Int.end + end -→ end. Similarly we have ?Int.end⊕?Real.end ⇓ ?3 because the action ?3 is always guaranteed independently of the internal choice, whereas ?Int.end ⊕ ?Real.end ⇓ ? √ 2 because ?Int.end ⊕ ?Real.end -→ ?Int.end and ?Int.end ⇓ ? √ 2. The previous definition induces two notions of convergence. Clearly convergence is a necessary condition for a session descriptor to have a dual. DEFINITION 2.3 (May and Must Converge). We say that η may converge, written η ↓, if for all η such that η =⇒ η -→ we have η ↓ µ for some µ. We say that η must converge, written η ⇓, if η ⇓ µ for some µ. As usual, we use η ↓ and η ⇓ to denote their respective negations.

Note that the two contractivity conditions of Definition 2.1 rule out behaviors involving infinite sequences of consecutive internal decisions. Therefore we will only consider strongly convergent processes, namely processes for which there does not exist an infinite sequence of -→ reductions.

The labeled transition system describes the subjective evolution of a session descriptor from the point of view of the process that uses a communication channel having that (residual) type. The last notion we need allows us to specify the evolution of a session descriptor from the dual point of view of the process at the other end of the communication channel. For example, we have ?Real.!Int.end + ?Int.!Bool.end ?3

-→ !Bool.end (the process receiving the integer value 3 knows that it has taken the right branch and now will send a Boolean value). However, the process sending the integer value 3 on the other end of the communication channel does not know whether the receiver has taken the left or the right branch, and both branches are actually possible. From the point of view of the sender, it is as if the receiver will behave according to the session descriptor !Int.end ⊕ !Bool.end, which accounts for all of the possible states in which the receiver can be after the reception of 3. The objective evolution of a session descriptor after an action µ is defined next. For example, (?Real.!Int.end+?Int.!Bool.end) ?3 = !Int.end⊕ !Bool.end but (?Real.!Int.end+?Int.!Bool.end) ? √ 2 = !Int.end. Note that η µ is well defined because there is always a finite number of residuals η such that η µ =⇒ η . This is a direct consequence of the contractivity conditions on session descriptors.

We now have all the ingredients for formally defining duality.

DEFINITION 2.5 (Duality). Let the dual of a label µ, written µ, be defined by: (i) = ; (ii) †v = †v; (iii) †η = †η; where ! = ? and ? = !. Then η1 η2 is the largest symmetric relation between session descriptors such that one of the following condition holds:

1. η1 ⇓ and η2 ⇓ ; 2. η1 ↓ and η1 ↓ µ implies η2 ⇓ µ and η1 µ η2 µ for every µ.

The intuition behind the above definition is that a dual must accept every input that its partner may output, or they must both agree on termination. For example, we have ?Real.!Int.end + ?Int.!Bool.end !Int.?(Int ∨ Bool).end, but ?Real.!Int.end + ?Int.!Bool.end !Int.?Int.end because the descriptor on the right is not sure that its partner will answer with an integer. However ?Real.!Int.end + ?Int.!Bool.end !(Real \ Int).?Int.end. As another example, we have ?Int.end ⊕ ?Real.end !Int.end because ?Int.end ⊕ ?Real.end ⇓ ?v for every v ∈ Int, however ?Int.end ⊕ ?Real.end ! √ 2.end because ?Int.end ⊕ ?Real.end ⇓ ? √ 2.

The reader may have observed that there is a circularity in the definitions of duality and of the labeled transition system. This is evident in rules (TR9-TR10) since the rules emit a dual of the sieve; that is, the relation η ∈ χ is defined in terms of χ whose definition is given in terms of the duality relation. Less evident is the circularity of rules (TR7-TR8), which resides in the fact that these rules emit values of a given type; if this type has the form begin.η, then its values are all the channels of the form c begin.η such that θ η implies θ η for all θ (cf. equation [START_REF] Castagna | A gentle introduction to semantic subtyping[END_REF] ): so also the definition of the relation v ∈ t depends on that of duality. The following theorem proves that this circularity is not one. THEOREM 2.6 (Well-foundness). The definitions of η ∈ χ, v ∈ t and η η are well founded.

PROOF. Thanks to condition 3 of Definition 2.1 recursion cannot enter descriptor prefixes (the condition that α.η is not a subtree of α). Therefore it is relatively easy to stratify the previous definitions. In particular let us define a weight as follows: a type has weight 0 if it does not contain session types; a descriptor has weight 0 if it contains just possibly empty sums of end; a type has weight i + 1 if the session types occurring in it are on descriptors of weight at most i; a descriptor is of weight i + 1 if the prefixes occurring in it are of weight at most i (here is where the condition 3 ensures that this definition is well founded for all session types). Next we define a weight for each relation we introduced so far: each η µ -→ η and η -→ η has weight 0 if it uses only axioms (i.e., (TR1) and (TR2)) and has weight i + 1 if it is proved by using relations of weight at most i; η µ has weight i if it is defined by reductions of weight at most i (we consider the successor as a binary relation); may/must actions/convergences relations and the duality relation all have weight i if they are proved by using relations of weight at most i. Finally, let us first define v ∈ t to be of weight 0 if t is of weight 0; then notice that both η ∈ χ and v ∈ t for t of weight at least 1 (cf. equation ( 7)) are defined in terms of duality: we then assign to each of them the greatest weight of the duality relations used in their definition.

Using this weight it is easy to check that the definitions in this section are well founded. A corollary of this theorem is that the definitions of subsessioning η ≤ η and subsieving χ ≤ χ (the former being a special case of the latter) given by the equation (6) in Section 2.2.1 are well founded as well.

The notion of duality is also a useful tool for better understanding the semantics of session descriptors. Let us revisit part of the LTS in the light of duality: Output of values. Rules (TR7-TR8) in Section 2.2 state that a descriptor is ready to respectively input and output some value of type t. The use of single values in labels may appear at first look surprising, as one would expect to see labels pretty similar to the fired actions. If we stated, say, that ?t.η emits ?t and !t.η emits !t (or, to be more liberal, ?t and !t with t <: t), then we would obtain quite a different semantics. In particular, it would no longer be possible to prove the following equations (where "=" denotes the equality induced by the relation ≤):

?(t1 ∨ t2).η = ?t1.η + ?t2.η (8) !(t1 ∨ t2).η = !t1.η + !t2.η (9) !(t1 ∨ t2).η = !t1.η ⊕ !t2.η (10)
In particular, the right hand-sided descriptors would no longer be smaller than the left hand-sided ones. Consider for example an instance of (9) where we take t1 ≡ Int and t2 ≡ Bool (here and henceforward we use "≡" to denote syntactic equality). It is clear that the two descriptors in the equation share the same set of duals (that is, they have the same semantics): the duals of both descriptors are descriptors that accept both an integer and a Boolean and then are dual of η. With the current definition of the LTS this holds true: whatever signal the left hand descriptor emits will be matched by every dual of the right hand since, in both cases, these signals will be on values of type Int∨Bool. Here is where the strong disjunction property on union types (5) is used: the left hand descriptor cannot emit a value that is neither an Int nor Bool. If the transition system had emitted types rather than values, then the duals of the right hand descriptor would not be able to match the signal !(Int ∨ Bool) since each summand of the right hand descriptor could at most emit Int or Bool. We could have introduced some extra definition of sets of emitted signals and saturated these sets with unions for internal and external sums, but the current solution avoids all this clutter. A similar reasoning holds for rules (TR9-TR10) because of the disjunction property we are going to prove next.

Internal choices, intersections, and disjoint unions. Using the definition of duality it is easy to see that η ⊕ η = η ∧ η since the duals of an internal choice must comply with both possible choices and thus be duals of both of them. Using this property it is easy to prove that sieves satisfy a disjunction property even stronger than the one for types, as the disjunction holds not only for single elements but for all the subsets of a union:

PROPOSITION 2.7. θ ≤ χ1 ∨ χ2 ⇐⇒ θ ≤ χ1 or θ ≤ χ2.
PROOF. Suppose that (⇒) does not hold (the converse is trivial). Then there exists a descriptor η1 dual of θ, such that η1 ∈ χ1 and η1 ∈ χ2, and a descriptor η2 dual of θ, such that η2 ∈ χ1 and η2 ∈ χ2. Now consider η1 ⊕ η2: since the semantics of an internal choice is the intersection of the duals of the choices, and θ is dual of both η1 and η2, then θ is dual of η1 ⊕ η2. But for the same reason we deduce that η1 ⊕ η2 ∈ χ1 and η1 ⊕ η2 ∈ χ2, and thus η1 ⊕ η2 ∈ χ1 ∨ χ2 by definition, yielding a contradiction. This property is essential to prove decidability of ≤.

A similar property holds for types of the form begin.η:

PROPOSITION 2.8. begin.η <: begin.η1 ∨ begin.η2 ⇐⇒ begin.η <: begin.η1 or begin.η <: begin.η2 PROOF. Recall that begin.η = {c begin.η | begin.η <: begin.η} (we cannot yet assume that begin.η <: begin.η implies η ≤ η). Take any channel of the form c begin.η . By the strong disjunction property (equation ( 5)) c begin.η ∈ begin.ηi for some i in [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF][START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF]. But by applying the definition of the semantics of session types to begin.ηi, this implies that for that i, begin.η <: begin.ηi.

Irrevocable outputs. By making external choices on output actions behave as internal ones, rules (TR5-TR6) state that outputs are irrevocable. This design choice was already explained in Section 2.2. In terms of duality, this choice corresponds to deciding whether, say, the external choices !Int.end+?Bool.end and ?Int.end+!Bool.end are to be considered as dual. In our setting the answer is negative as we consider that outputs may be asynchronously emitted even for external choices, therefore the two partners can get stuck if both decide to emit their outputs. This behavior is a direct consequence of rules (TR5-TR6). As we discuss in the conclusion of this presentation, this is not the only reasonable answer. For instance, we could suppose that in a case such as the above one, the two partners perform some form of handshake to decide which one will perform the output; in that case rules (TR5-TR6) should be removed. We chose not to do so since the "irrevocable inputs" solution seems better fit a wide area network usage scenario.

Subtyping

Now that we have defined the duality relation, and therefore subsessioning, we can also formally define the subtyping relation. The types defined in Section 2.1 include three type combinators (union, intersection, and negation), one type constructor begin.η, plus other basic types and type constructors (inherited from the host language) that we left unspecified (typically, Real, Bool, ×, . . . ). We define the subtyping relation semantically using the technique defined in [START_REF] Frisch | Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types[END_REF] and outlined in Section 2.2.1, according to which types are interpreted as the set of their values, type combinators are interpreted as the corresponding set-theoretic operations, and subtyping is interpreted as set containment. As a consequence, testing a subtyping relation is equivalent to testing whether a type is empty, since by simple set-theoretic transformations we have that t1 <: t2 if and only if t1 ∧ ¬t2 <: ∅ (where we use ∅ to denote the empty type, that is the type that has no value). Again by simple settheoretic manipulations, every type can be rewritten in disjunctive normal form, that is a union of intersections of types. Furthermore, since type constructors are pairwise disjoint (there is no value that has both a session type and, say, a product type-or whatever type constructor is inherited from the host language), then these intersections are uniform since they intersect either a given type constructor, or its negation (see [START_REF] Castagna | A gentle introduction to semantic subtyping[END_REF][START_REF] Frisch | Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types[END_REF] for details). In conclusion, in order to define our subtyping relation all we need is to decide when

W k∈K ( V i∈I k begin.ηi ∧ V j∈J k ¬begin.ηj) <: ∅. Since
M i∈I ηi ≤ ηj (11)
Note that when in the equation above I and J are singletons it reduces to begin.η1 <: begin.η2 ⇐⇒ η1 ≤ η2 that is the form discussed at the end of Section 2.2.1.

Coinductive characterizations

The subsessioning relation defined in terms of duality embeds the notion of safe substitutability because of its very definition, but it gives little insight on the properties enjoyed by ≤. This is a common problem of every semantically defined preorder relation based on tests, such as the well-known testing preorders [START_REF] De Nicola | Testing equivalences for processes[END_REF] (the set of duals of a descriptor can be assimilated to the set of its successful tests). In order to gain some intuition over ≤ and to obtain a useful tool that will help us studying its properties we will now provide an alternative coinductive characterization. Before doing so, we need to characterize the class of descriptors that admit at least one dual. Recall that η is viable if there exists η such that η η . Any non-viable descriptor is the least element of ≤, which henceforward will be denoted by ⊥.

DEFINITION 2.9 (Coinductive Viability). η is the largest predicate over descriptors such that either 1. η ↓ and η ↓ µ implies η µ for every µ, or 2. there exists µ such that η ⇓ µ and η µ .

The definition provides us with a correct and complete characterization of viable descriptors, as stated in the next proposition, which is proved in Appendix A.2.

PROPOSITION 2.10. η if and only if η is viable.

We can now read the statement of Definition 2.9 in the light of the result of the above proposition: Definition 2.9 explains that a descriptor is viable if either (1) it emits an output action regardless of its internal state and every successor after every possible output action is viable too or (2) it guarantees at least one input action such that the corresponding successor is viable too. DEFINITION 2.11 (Coinductive Subsession). η η is the largest relation between session descriptors such that η implies η and 1. η ⇓ and η ↓ µ imply η ↓ µ with η µ η µ , and 2. η ⇓ µ and η µ imply η ⇓ µ with η µ η µ , and 3. η ↓ and η ⇓ imply η ↓ and η ⇓ .

The definition states that any viable descriptor η may be a subsession of η only if η is also viable. This is obvious since we want the duals of η to be duals of η as well. Furthermore, condition [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF] requires that any output action emitted by the larger descriptor must also be emitted by the smaller descriptor, and the respective continuations must be similarly related. This can be explained by noticing that a descriptor dual of η in principle will be able to properly handle only the outputs emitted by η; thus in order to be also dual of η it must also cope with η outputs, which must thus be included in those of η, hence the condition. The requirement η ⇓ makes sure that η really emits some output actions. Without this condition we would have ?Int.end ?Int.end + end as the descriptor on the r.h.s. emits which is not emitted by the l.h.s. However, it is trivial to see that ?Int.end ?Int.end + end. Condition (2) requires that any input action guaranteed by the smaller descriptor must also be guaranteed by the larger descriptor. Again this can be explained by noticing that a descriptor dual of η may rely on the capability of η of receiving a particular value/descriptor in order to continue the interaction without error. Hence, any guarantee provided by the smaller descriptor η must be present in the larger descriptor η as well. The additional condition η µ considers only guaranteed input actions that have a viable dual, for a guaranteed input action with a nonviable dual is practically useless. Without such condition we would have, for instance, that ?Int.!∅.end + ?Bool.end ?Bool.end, because the descriptor on the l.h.s. guarantees the action ?3 which is not guaranteed by the descriptor of the r.h.s. of . It is clear however that in this case the subsessioning relation must hold since the l.h.s. and r.h.s. have the same set of duals. Finally, condition (3) captures the special case in which a descriptor emitting output actions (η ↓) is smaller than a descriptor guaranteeing input actions (η ⇓). This occurs only when η may internally decide to terminate (η ↓ ) and η guarantees termination (η ⇓ ). In this case, every dual of η must be ready to terminate and to receive any output action emitted by η, hence it will also be dual of η which guarantees termination but does not emit any output action.

We end this subsection by stating that the coinductive and the semantic definitions of subsessioning coincide, so from now on we will use ≤ to denote both. The proof of this theorem is the content of A.3. THEOREM 2.12. η1 η2 ⇐⇒ η1 ≤ η2.

Properties of the subsession relation

Table 1 shows some relevant rules regarding ≤ Aside from providing further insight on the properties of ≤, these rules are also used in the following for proving the existence of the normal forms for session descriptors and the correctness of the algorithms. In the table we write ∅ to denote either ∅ (the empty type) or ⊥ (the least sieve) according to the context.

Rules (E1-E8) state the fundamental properties of the external choice operator. Rules (E1-E4) are trivial being the usual idempotency, commutativity, associativity and distributivity laws of exter-

(E1) η + η = η (E2) η + η = η + η (E3) η + (η + η ) = (η + η ) + η (E4) η + (η ⊕ η ) = (η + η ) ⊕ (η + η ) (E5) α.η + α.η = α.(η ⊕ η ) (E6) ?t.η + ?s.η = ?(t ∨ s).η (E7) ?χ.η + ?χ .η = ?(χ ∨ χ ).η (E8) η + ⊥ = η (I1) η ⊕ η = η (I2) η ⊕ η = η ⊕ η (I3) η ⊕ (η ⊕ η ) = (η ⊕ η ) ⊕ η (I4) η ⊕ (η + η ) = (η ⊕ η ) + (η ⊕ η ) (I5) α.η ⊕ α.η = α.(η ⊕ η ) (I6) ?t.η ⊕ ?s.η = ?(t ∧ s).(η ⊕ η ) (I7) ?χ.η ⊕ ?χ .η = ?(χ ∧ χ ).(η ⊕ η ) (I8) η ⊕ ⊥ = ⊥ (B1) ?ψ.η = ⊥ (ψ = ∅) (B2) !ψ.η = ⊥ (ψ = ∅) (B3) ?t.η ⊕ ?χ.η = ⊥ (B4) ?ψ.η ⊕ !ψ .η = ⊥ (B5) ?ψ.η ⊕ end = ⊥ (O1) !ψ.η + end = !ψ.η (ψ = ∅) (O2) !ψ.η + ?ψ .η = !ψ.η (ψ = ∅) (O3) !ψ.η + !ψ .η = !ψ.η ⊕ !ψ .η (ψ, ψ = ∅) (O4) !t.η ⊕ !s.η = !(t ∨ s).η (t, s = ∅) (O5) !χ.η ⊕ !χ .η = !(χ ∨ χ ).η (χ, χ = ⊥) (S1) ?t.η ≤ ?(t ∨ s).η (S2) ?χ.η ≤ ?(χ ∨ χ ).η (S3) !(t ∨ s).η ≤ !t.η (t = ∅) (S4) !(χ ∨ χ ).η ≤ !χ.η (χ = ⊥) (S5) η ⊕ η ≤ η
Table 1. Selected equalities and inequalities.

nal choices. Rule (E5) shows that an external choice may actually hide an internal choice if it combines descriptors having a common prefix. This is a well-known axiom in the testing theories [START_REF] De Nicola | Testing equivalences for processes[END_REF] and it also shows that the external choice does not coincide with the set-theoretic union operator (the internal choice, on the other hand, does coincides with the set-theoretic intersection). Rule (E6) shows the interaction between input actions (over types) and the external choice operator: the value received from the channel is chosen externally, it cannot be negotiated by the receiver. Rule (E7) is similar to rule (E6), except that it deals with sieves. Rule (E8) states that ⊥ is the neutral element of the external choice. Rules (I1-I9) state the fundamental properties of the internal choice operator. Rules (I1-I4) are similar to rules (E1-E4). Rule (I5) is the distributivity law of the prefix operator over the internal choice (the same law does not hold for the external choice operator). Rule (I6) shows the interaction between input actions over types and the internal choice operator. A dual of the descriptor on the l.h.s. of = does not know whether the descriptor is ready to receive a value of type t or of type s. Thus, the only possibility is to send a value that has both types. As a consequence, if t and s are disjoint types, namely if t ∧ s = ∅, then both descriptors are ⊥ (see rule (B1) below). Rule (I7) is similar to rule (I6), except that it deals with sieves. A dual of the descriptor on the l.h.s. of = does not know whether the descriptor is ready to receive a descriptor θ such that θ is dual of χ or such that θ is dual of χ . Thus, the only possi-bility is to send a descriptor that is dual of both θ and θ . Rule (I8) states that ⊥ is the absorbing element of the internal choice.

Rules (B1-B5) characterize non-viable descriptors, namely those descriptors that have no dual. Rules (B1-B2) deal with communications of values from empty types and delegations of sessions with non-viable descriptors. Since these descriptors are completely inert (they do not emit any visible action), they are comparable to the canonical non-viable descriptor ⊥. Rule (B3) states the disjunction between values and descriptors: no value is a descriptor, and no descriptor is a value. Rule (B4) states the directionality of our communication model. In order to be viable, a descriptor cannot simultaneously allow both input and output actions. The only exception to this rule is when the output actions are offered in an external choice, see rules (O1-O3) below. Rule (B5) is similar to rule (B4), except that it deals with end and input actions.

Rules (O1-O5) characterize the peculiar properties of output actions. In every rule the side condition ensures that the output action is not inert (see rule (B2) above). Rules (O1-O2) state that an output action composed in external choice with a end or an input action preempts the alternative action. Rule (O3) states that external and internal choices of output actions are indistinguishable, since these actions are irrevocable. Rule (O4) shows the interaction between output actions over types and the internal choice operator: the value sent over the channel is decided internally by the sender, it will not be negotiated with the receiver. Rule (O5) is similar to rule (O4), except that it deals with sieves.

Rules (S1-S2) show the standard covariant property of inputs: the duals of a session that is capable of receiving values of type t will also be duals of a session that is capable of receiving more values. Rule (S2) is similar to rule (S1) except that it deals with input of descriptors and it can be explained in the same way using the intuition that sieves stand for the set of their duals. Rules (S3-S4) complement rules (S1-S2) with dual properties for output actions, where we have contravariance. Note that in both cases we need one extra hypothesis, namely that t = ∅ and χ = ⊥. This guarantees that the larger descriptor will actually output some value/descriptor whenever the smaller one does so.

Finally, rule (S5) states that the duals of some session are also duals of a more deterministic session. In the testing theories for processes this law characterizes the deadlock sensitive must preorder.

We conclude this section with two remarks. First of all, the rules of Table 1 allow us to derive the following decomposition laws:

?t.η + ?s.η = ?(t \ s).η + ?(s \ t).η + ?(t ∧ s).(η ⊕ η ) !t.η ⊕ !s.η = !(t \ s).η ⊕ !(s \ t).η ⊕ !(t ∧ s).(η ⊕ η )
the latter rule holding when none of the sets t \ s, s \ t, and t ∧ s is empty. Similar rules can be derived for inputs and outputs of sieves, as opposed to types. These rules play a fundamental role in all the algorithms that will follow because they allow us to rewrite external and internal sums so that every summand of the sum begins with a prefix that is disjoint from (emits labels that are not emitted by) the prefix of any other summand.

The second remark concerns the interaction of ≤ with the operators of session descriptors. It is easy to see that ≤ is preserved by the prefix and the internal choice operators. In the latter case, this follows from the fact that ⊕ coincides with the intersection operator in the set-theoretic interpretation of session descriptors. However, as we have already seen while discussing rule (E5), + does not correspond to a Boolean operation and this ultimately makes + quite subtle, as ≤ is not respected by + in general 2 is useless. However, removing this capability may also remove interferences in the context of an external choice, making (I6) unsafe in general.

Finally, rule (B4) must be used with care within an external choice because its output capability makes the descriptor on the l.h.s. of = to be observable (it may autonomously emit an action), whereas ⊥ is totally inert. For instance we have ?Int.end⊕!Int.!∅.end = ⊥ and ⊥+?Bool.!3.end = ?Bool.!3.end, but (?Int.end ⊕ !Int.!∅.end) + ?Bool.!3.end = (?Int.end + ?Bool.!3.end) ⊕ (!Int.!∅.end + ?Bool.!3.end) = ⊥. Rule (B5) suffers from a similar problem, which is slightly less severe because end denotes a terminated descriptor.

Algorithms

In order to use our type system we must be able to decide the relations we introduced in the previous sections, namely subsieving (and subsessioning), subtyping, and duality.

Subsieving. Let us start to show how to decide that a sieve is smaller than another. Since Boolean combinators have a settheoretic interpretation we can apply exactly the same reasoning we did for types in Section 2.3. Namely, deciding χ ≤ χ is equivalent to deciding χ ∧ ¬χ ≤ ⊥. The l.h.s. can be rewritten in disjunctive normal form whose definition for sieves is (we convene that , where for all i ∈ I, ψi = ∅, ψi and ηi are in strong normal form and for all i, j ∈ I, i = j implies ψi ∧ ψj = ∅, and end is possibly missing.

W i∈∅ χi = P i∈∅ ηi = ⊥): DEFINITION 2.
The following theorem proves that every sieve can be effectively transformed in strong normal form. Its proof, which is done by simultaneous induction with that of Theorem 2.18 later on, is the content of Appendix A.1. THEOREM 2.15 (Normalization). For every sieve χ it is possible to effectively construct χ in strong normal form such that χ = χ .

Finally, to check that two descriptors are in relation we rewrite both of them in strong normal form, check that neither is ⊥, and then apply the algorithm whose core rules are given in Table 2.

Table 2.

(END)

end ≤ end

(PREFIX) η ≤ η α.η ≤ α.η (MIX-CHOICES) M i∈I ηi ⊕ end ≤ X j∈J η j + end (EXT-CHOICES) I ⊆ J ηi ≤ η i (∀i∈I) X i∈I ηi ≤ X j∈J η j (INT-CHOICES) J ⊆ I ηj ≤ η j (∀j∈J) M i∈I ηi ≤ M j∈J η j
Table 2. Algorithmic subsessioning structural rules.

Rule (MIX-CHOICES) states that an internal choice is smaller than an external one if and only if they both have an end summand. Rule (EXT-CHOICES) states that it is safe to widen external choices whereas rule (INT-CHOICES) states that it is safe to narrow internal ones. Both rules are used in conjunction with (PREFIX), which states covariance over descriptor continuations. Note that rule (PREFIX) relates two descriptors only if they have the same prefix. Therefore before applying (EXT-CHOICES) and (INT-CHOICES) we have to transform the descriptors so that prefixes on the two sides that have a non-empty intersection are rewritten in several summands so as to find the same prefix on both sides: this is done by the rules in Table 14 in Appendix A.1. These rules perform repeated applications of the decomposition laws described in Section 2.5.

The soundness and completeness of the algorithm need two preliminary results. The first one states that no finite union of session descriptors covers the whole S . Namely, it is always possible to find another η having at least one dual descriptor that is not dual of any of the descriptors in the finite union. LEMMA 2.16. For every viable sieve of the form W i∈I ηi, there exists a descriptor η such that

W i∈I ηi ∨ η ≤ W i∈I ηi.
PROOF. By induction on the cardinality of I. We just consider the case for |I| = 1, that is W i∈I ηi ≡ η , the result follows by straightforward induction. Consider the set {θ | η =⇒ θ -→}. Now choose any value v such that for all θ in this set θ

!v -→ implies that there exists v = v such that θ !v -→.
Note that such a v always exists because no descriptor can emit infinitely many singleton types (indeed if from a stable form a session type can emit just one output value, then this means that the output is on the singleton containing that value). Then setting η ≡ !v.end proves the result.

The second auxiliary result simply states the correctness of rule (PREFIX) generalized to a finite number of prefixes. LEMMA 2.17. For all α1, . . . , αn, η, η , if η ≤ η , then α1.

• • • αn.η ≤ α1. • • • αn.η .
PROOF. By examination of the coinductive characterization of ≤ (Definition 2.11) it is easy to check that the result holds for n = 1. The whole result follows from a straightforward induction on n. THEOREM 2.18 (Soundness and Completeness). The algorithm is sound and complete with respect to ≤ and it terminates.

Duality. Duality can be reduced to subsessioning since η η if and only if η ≤ η , where we write η for the canonical dual of η, namely the least descriptor in the set-theoretic interpretation of η. Computing η is trivial once η is in strong normal form (see Theorem 2.15): it suffices to change every ? into !, every + into ⊕ and viceversa, and to coinductively apply the transformation to the continuations leaving end descriptors unchanged. Regularity ensures that the transformation terminates (by using memoization techniques) and showing that the obtained session descriptor is the canonical dual of η is a trivial exercise.

Typing

In the following section we first show how the session type theories discussed in various papers fit in our framework, and then we type a π-calculus and an object-oriented calculus in order to show the flexibility and espressivity of our approach.

Expressing existing session type theories

All monomorphic dyadic session type theories proposed in the literature are particular cases of the session descriptors discussed here.

The first version of session descriptors can be traced back to the seminal work of Honda, Vasconcelos, and Kubo [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF] in the context of process algebras. In the same context [START_REF] Bonelli | [END_REF] enhances sessions with correspondence assertions. Later on Vasconcelos, Gay, and Ravara have extended the approach to multithreaded functional languages [START_REF] Vasconcelos | Typechecking a Multithreaded Functional Language with Session Types[END_REF]. In all these works session descriptors embed two n-ary operators for internal and external choice, which are strictly coupled with the communication of labels that indicate the selected branch in a choice. The session descriptors of [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Bonelli | [END_REF][START_REF] Vasconcelos | Typechecking a Multithreaded Functional Language with Session Types[END_REF] can be written in our model as follows:

η ::= end | α.η | L i∈I ! i.ηi | Σi∈I ? i.ηi α ::= !t | ?t | !η | ?η
where we consider labels as singleton types. The same syntax can be used to describe the session descriptors developed for CORBA [START_REF] Vallecillo | Typing the Behavior of Objects and Components using Session Types[END_REF], Boxed Ambients [START_REF] Garralda | BASS: Boxed Ambients with Safe Sessions[END_REF], and the ones used to type the Conversation Calculus [START_REF] Caires | Conversation Types[END_REF]. To draw a parallel with sequential languages, to pass from the systems above to our framework is like passing from a language with labels and records, in which the selection of the code to be executed is driven by the label received, to a language with dynamically resolved overloaded functions in which the code is selected according to the type of the received value.

In the context of object-oriented languages, session type theories assuring type safety and progress were investigated in MOOSE [START_REF] Dezani-Ciancaglini | Session Types for Object-Oriented Languages[END_REF], AMOOSE [START_REF] Coppo | Asynchronous Session Types and Progress for Object-Oriented Languages[END_REF], and MOOSE<: [START_REF] Dezani-Ciancaglini | Bounded session types for object-oriented languages[END_REF]. The syntax of all session descriptors discussed in the above papers, but for [START_REF] Dezani-Ciancaglini | Bounded session types for object-oriented languages[END_REF] where bounded polymorphism is considered, are special cases of our model, after identifying recursive types with their infinite unfolding. More specifically, the syntax of the session descriptors in [START_REF] Dezani-Ciancaglini | Session Types for Object-Oriented Languages[END_REF] and [START_REF] Coppo | Asynchronous Session Types and Progress for Object-Oriented Languages[END_REF] can be reduced to:

η ::= end | α.η | !true.η ⊕ !false.η | ?true.η + ?false.η α ::= !t | ?t | !η | ?η
since these works deal with sessions where branching is controlled by means of boolean conditions.

A calculus that amalgamates the notion of session-based communication with the one of object-oriented programming is presented in [START_REF] Capecchi | Amalgamating Sessions and Methods in Object Oriented Languages with Generics[END_REF][START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF]. In these works sessions and methods are unified, channels are implicit, and delegation is realized by means of session calls. Branching is determined by the runtime type of the ob-ject being communicated. Session descriptors with this form of dependencies can be written very naturally in our model as:

η ::= end | L i∈I !Ci.ηi | Σi∈I ?Ci.
ηi where Ci are class names in [START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF] and generic class names in [START_REF] Capecchi | Amalgamating Sessions and Methods in Object Oriented Languages with Generics[END_REF]. The cited works hardcode different selection policies for branching. We can easily reproduce them all by using Boolean combinators on classes.

π-calculus

The most interesting observation on process typing is that with our framework sessions can be typed in the standard π-calculus with internal/external choices and bound/free outputs (with the single modification on the type-based selection of external choices we described in the introduction), without primitive operators tailored to session-based communications (in the spirit of Kobayashi's [26]). The intuition is that bound outputs, written c!(x : η), are session initiations where c is the public channel of the session and x the session private channel of descriptor η; free outputs are reserved for session communications/delegations, and inputs are either session communications or session connections according to whether they are meant to synchronize with free or bound outputs, respectively. For example, the following process models a node that handles communications described by a protocol η and delegates communications described by unknown protocols to a sibling node, in a token-ring fashion: NODE(mypublicname, nextpublicname, η, P ) = mypublicname?(x : ? .end). The node waits for a connection on its public channel mypublicname and, once the connection is made, catches on the established session channel x a delegated session y of an arbitrary descriptor ( is the top sieve). If the delegated session is of protocol η (this is checked by using an external choice), then the node handles the session in the process P , otherwise it connects to a sibling node nextpublicname (via a bound output) and delegates y to it (via a free output). Both mypublicname and nextpublicname are public channels of type begin.! .end. Under these hypotheses and provided that y is used in P according to η, the process above result typable by the type system given right after the formal definision of PIC syntax and semantics we present next.

Syntax and semantics

The main design criterion for our process calculus PIC is minimality and similarity to π-calculus: we define the smallest calculus that allows us to use all the characteristics of our session types. The syntax is given in Table 3. It is a π-calculus with internal and external choices, free outputs on bound channels and bound outputs on free channels respectively denoted by h!e and a!(x : η). Processes are the possibly infinite regular trees that are generated by the productions in Table 3 and that satisfy the contractivity condition requiring that on every infinite branch there are infinitely many applications of the prefixed process. Contractivity rules out processes of the form, e.g., P = P ⊕ P and-as for types-it provides an induction principle based on the Noetherian relation P1 + P2 Pi and P1 ⊕ P2 Pi .

The calculus does not include restrictions or parallel composition. Parallel composition is present only at the upper level of systems where session conversations take place. We do not need explicit restriction, those implicitly defined in bound outputs are 3. Syntax of PIC processes and systems.

enough 3 and are implemented resorting to internal channels, denoted by k. These appear greyed in the productions to stress that such channels occur only at runtime (they cannot be written by the programmer but they are generated at session connection). We assume that "˜" is a bijective mapping from internal channels to internal channels with k = k and that is an involution (i.e., k = k, a technique quite common in calculi for sessions). We say that k and k are dual. Dual channels represent the two end-points of a session. Besides internal channels, expressions include channel variables (ranged over by x), channel values (that is session public names, ranged over by c and tagged by their smallest type, which is of the form begin.η to enforce the strong disjunction property ( 5)), and the expressions of the host language (represented in the productions by dots). We use v to range over both channel values and host language values and suppose given the relation v ∈ t that associates each host language value with its types and each channel value with the types larger than or equal to its tag. The set of labels is defined by

::= τ | n?(x : ψ) | k!m | c t !(x : η)
where

m ::= v | k n ::= c t | k
These are already quite informative. They tell us that synchronization can happen only on closed channels (and not on variables ranging over channels), that is private channels for communication and public channels for session connection. Also bound outputs can send only closed expressions (ranged over by m, that is values and private channels: the latter are not values though they operationally behave like them, since they are not associated to a type). Public channels appear tagged also in labels: though this tagging is not used it allows us to have more compact rules.

The labelled transition rules for processes are straightforward and they can be found in Table 4. They handle the irrevocability of outputs and compute expressions before synchronization. The semantics of systems is the standard π-calculus semantics apart the two points we evoked before, namely that outputs are irrevocable and that selection for external choices is based on the type of the arguments. This last point is showed by the synchronization rules for system presented in Table 5, more in particular in the last two rules where synchronization takes place only if the objects of the outputs match the types/sieves of the input. Note also that a new session is started (rule CONNECTION) when a bound output is performed on a channel value, in that case a new pair k, k of internal channels is spawned. Finally note that the dynamic checks in the last two rules are needed and used to drive the computation, since external choices are dynamically selected by using the type of the communicated value, or the descriptor of the delegated session. 3 We could have introduced at system level restrictions restrictions of the form (νc : begin.η) so as to declare public session channels, limit their scope, and avoid explicit public channel tagging. We preferred to focus on a slightly simpler calculus.

-→ P R-CONNECT c t !(x : η).P c t !(x:η) -→ P R-INTCH P ⊕ Q τ -→ P R-EXTINT P τ -→ P P + Q τ -→ P + Q R-EXTSEND P k!m -→ P P + Q τ -→ P R-EXTCH P -→ P = τ P + Q -→ P Table 4
. PIC process reduction rules.

LIFT

P -→ P Σ P -→ Σ P PAR Σ S -→ Σ S Σ S T -→ Σ S T CONNECTION Σ S c t !(x:η) -→ Σ S Σ T c t ?(x:η ) -→ Σ T k ∈ dom(Σ) Σ S T τ -→ Σ, k : η, k : η S [ k /x] T [ k/x] COMMUNICATION Σ S k!v -→ Σ S Σ T k?(x:t) -→ Σ T v ∈ t Σ, k : η, k : η S T τ -→ Σ, k : η !v , k : η ?v S T [ v /x] DELEGATION Σ S k!k -→ Σ S Σ T k?(x:χ) -→ Σ T Σ(k ) ≤ χ Σ, k:η, k:η S T τ -→ Σ, k:η !Σ( k ) , k:η ?Σ( k ) S T [ k /x]
Table 5. PIC system reduction rules.

We adopt the standard conventions of using

Typing of PIC

The original motivation for introducing session types [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF] was to ensure that values sent and received in communication protocols were of appropriate types and that the two partners always agreed on how to continue the conversation. A type system ensuring also the progress property, i.e., that a started session cannot get stuck if the required connections are available, was first proposed in [START_REF] Dezani-Ciancaglini | A distributed object oriented language with session types[END_REF].

In the present calculus, as in [START_REF] Dezani-Ciancaglini | Bounded session types for object-oriented languages[END_REF], the operational semantics itself ensures that there cannot be a type mismatch in communications, since all checks are performed at the moment of the synchronisation. So for example the system k!3 k?(x : Bool) is stuck. We present in this section a type system which prevents also any deadlock due to the interleaving of two or more sessions.

More precisely we want to ensure that whenever a well-typed system is stuck (i.e., it cannot perform any internal reduction) it is because either all its processes have successfully terminated or at least one of them is on hold on a connection request. This means that whenever a session is started, if it does not perform any further connection, then either it eventually successfully terminates, or it continues to interact (recall that both process and session descriptors may be recursive). More formally: -→ .

Our process calculus is so close to the syntax of the session descriptors that it is not difficult to imagine how to map a given channel to its session type. For instance, consider the process c t !(z : η).z!(3).z?(x : Real).(z!(x) ⊕ z!(true)) which opens a connection on c in which it writes an integer, reads a real, and then decides whether to send back the received real or a Boolean value. It is clear that such a process is well typed when η =!Int.?Real.(!Real.end ⊕ !Bool.end) and t is (a subtype of) begin.η. However, in order to ensure the progress property, the way in which a process uses different sessions must be quite limited. Once a connection is established, and a private channel, which we call current session, is spawned, then the process can act according to (combinations of) the following options:

1. establishing a new connection;

2. performing a communication on the current session;

3. ending the current session by stopping using the corresponding channel (there is no explicit end in processes, so the end of a session is reached when its channel is no longer used);

4. delegating on the current session the innermost, not ended, enclosing session;4 the process stops using the delegated session;

5. receiving a delegated session and using it in the continuation as the current session.

Such restrictive behaviour corresponds to using sessions as critical regions that forbid deadlocks on circular waits. Each critical region is associated with a particular internal channel: it is entered whenever this channel is received by delegation or started by a connect, it is closed when the channel is delegated or no longer used. Once a process has entered a critical region all it can do is to communicate on the channel associated with the region or to enter a new critical region. To see why these restrictions are necessary let us comment a couple of examples of deadlock.

Let t1 = begin.!Int.end, η1 =!Int.end and η2 =?Int.end. A first simple example of deadlock is given by c t 1 !(z1 : η1).b t 1 ?(z2 : η2).z2?(x : Int).z1!6 c t 1 ?(z3 : η2).b t 1 !(z4 : η1).z3?(x : Int).z4!5

After two executions of the CONNECTION rule, both processes starve waiting for values that are never sent. Note that the problem here is generated by the process that provides the service c (that is the second one) since it make a communication on (the private channel of) c before having ended the session it requested on b.

Internal and external sums can produce deadlocks since they can make choices unavailable as in c t 1 ?(z1 : η2).b t 1 ?(z2 : η2).z1?(x :

Int) + z2?(x : Int) c t 1 !(z3 : η1).z3!6 b t 1 !(z4 : η1).z4!5
and in the similar system obtained by replacing ⊕ to + . Another example is c t 1 ?(z1 : η3).z1?(x : Int) + b t 1 ?(z2 : η2).z2?(x : Int).z1?(x : Bool) c t 1 !(z3 : η1).z3!6 b t 1 !(z4 : η1).z4!5

where η3 = (?Int + ?Bool).end: note that the connection on b forbids the communication on the private channel created by the connection on c.

More subtle examples of deadlock spring from session delegation, whereby a (sequential) process can receive the dual of a chan-T-EXTCH

Γ * P : (h : η1 • ∆) Γ * Q : (h : η2 • ∆) Γ * P + Q : (h : η1 + η2 • ∆)
Table 6. Type system for PIC. nel it already owns, making synchronization impossible. Consider c t 1 ?(z1 : η2).b t 2 !(z2 : η4).z2!z1 c t 1 !(z3 : η1).

b t 2 ?(z4 : η5).z4?(x : η2).x?(y : Int).z3!6

where t2 ≡ begin.!(?Int.end).end, η4 =!(?Int.end).end, η5 = ?(?Int.end).end. This phenomenon may also jeopardise subject reduction, as discussed in [START_REF] Yoshida | Language primitives and type disciplines for structured communication-based programming revisited[END_REF]. Such problems can be avoided by resorting to the strict usage discipline we described earlier which is enforced by the typing discipline defined in Table 6. The judgements for processes have the forms Γ P : ∆ and Γ * P : ∆ where Γ is a type environment (a mapping from variables to types) and ∆ is a session stack. The latter is a mapping from private channels to session descriptors to which identifiers of ended sessions can be freely added (rule T-WEAK) and is used to record the session descriptors of the channels used in P. It is organised as a stack (the rightmost element being the top) to keep track of the current session, that is the most recently created one (i.e., in our analogy, the one associated with the current critical region). The stack allows us to avoid the first example of deadlock, by organising sessions as nested critical regions in which a channel cannot be used unless all nested sessions have been consumed (either because they ended or because they were delegated to some other process). Actions are allowed only if their subject is the current session channel, the one on the top of the stack

(rules T-CONNECT-REQUEST, T-CONNECT-ACCEPT, T-SEND, T-RECEIVE, T-SENDS, and T-RECEIVES

) and they are recorded in the conclusion. In addition, the rules for communication check that type constraints are satisfied while sieve constraints are checked by the delegation rules.

The rule T-CONNECT-ACCEPT hides several subtleties. If a process contains the action c begin.η ?(x : η).P it means that it provides the service c and it implements it by the process P. Note that in P the corresponding private channel implements a behaviour dual of the one that tags c. Therefore the tag of a public channel declares the behaviour that all clients of the service must follow. In other terms it describes the most demanding client this service is ready to serve. Also note that the typing rule imposes that the acceptance of a connect can only be written for an actual public channel and not for a variable of the corresponding type. This corresponds to the everyday practice that a service is associated to a particular URL instead of being dynamically bound to it (which does not prevent several processes to implement the same service) and enforces the assumption-we did in Section 2.2.1-that the only way to use a public service name is to call it. In other words, while the public names of services are first class and, as such, they can be passed around in communications, the only way to use them is to request a connection on them. Technically, this restriction allow us to avoid the use of polarities to type communications: because of the use of duality in the T-CONNECT-ACCEPT one should require contravariance for channels used for session acceptance, covariance for those used for session request and invariance for channels used in both cases. The solution we chose, besides being natural, correspond to enforcing invariance when accepting connections.

To deal with the deadlocks induced by sums we use the * judgements which assure that the processes in the conclusion offer communications just on the channel which is on the top of the stack. Two processes can be composed by means of an internal choice only if either are typed by exactly the same stack (rule T-INT) or by means of an internal or external choice if they differ for the typing of only one channel on which a communication is immediately available (rules T-INTCH, T-EXTCH). The example of deadlock due to delegation is avoided by requiring that the only other internal channel which can occur in a process accepting a delegation is the channel on which the delegation took place (rule T-RECEIVE). The typing discipline is lifted to systems by simply merging all channel assumptions, disregarding the order in which they appear (by means of the operator set), and obtaining in this way session environments, ranged over by Λ.

Since evaluation consumes session descriptors and adds fresh initial channels with their descriptors, we need to introduce a partial order on session stacks and session environments so that subject reduction can be formulated as follows. Progress clearly fails for systems which contain free variables or internal channels that are not properly paired. For this reason our typing can only assure progress for initial systems defined as follows: DEFINITION 3.4 (Initial system). A well-typed system is initial if it is the parallel composition of closed process where no internal channel occurs.

The proof of progress depends on the remark that the session environments in the operational semantics and in the typing of systems respectively give the objective and subjective views of the internal channel behaviours. For example consider the system S = k!3.k?(x : 2 ∨ 4) k?(y : 3). k!2 + k?(y : 3). k!4. We get {k : !3.?(2 ∨ 4).end, k : ?3.!2.end + ?3.!4.end} S τ -→ Σ S where Σ = {k : ?(2 ∨ 4).end, k : !2.end ⊕ !4.end} and S = k?(x : 2 ∨ 4) k!2, while S : {k : ?(2 ∨ 4).end, k : !2.end}. The descriptor of k in Σ is the internal choice between !2.end and !4.end, since an observer does not know if the value 3 was received by the process k?(y : 3). k!2 or by the process k?(y : 3). k!4. Instead the descriptor of k in the typing of S is !2.end, since the value 3 was received by the process k?(y : 3). k!2.

More precisely the session environments created in the operational semantics starting from an initial system assigns to internal channels equal or smaller descriptors than the session environments used in typing. This is the content of the following lemma which is a key in the proof of progress. An interesting consequence of the above lemma is fidelity of communications i.e., that once a session is started the communications are done in the expected order and exchange data of the expected types.

We state now the progress theorem whose proof is the content of Appendix B.2. THEOREM 3.6 (Progress). Every initial system satisfies the progress property.

It is interesting to note that if we disregard the order in the session stack (i.e., we use session environments in all the rules) and we allow an arbitrary session stack in the premise of rule T-RECEIVE, then we get a type system which still enjoys subject reduction but no longer guarantees progress.

An OO calculus

In this section we will show how we can naturally enhance the typing of [START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF] using the general session descriptors: in particular we will allow session overloading, i.e. the same session name can be declared with different session descriptors in a class hierarchy. At run time an appropriate session body will be chosen using the duality and subfiltering relations. As in the original paper we do not have cast and overriding, which are orthogonal to our approach. For simplicity we avoid to consider while commands.

Syntax of the OO calculus

The calculus of [START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF] is based on Featherweight Java [START_REF] Igarashi | Featherweight Java: a Minimal Core Calculus for Java and GJ[END_REF] (abbreviated with FJ). We use the standard convention of denoting with ξ a sequence of elements ξ1, ..., ξn.

Programs are defined from a collection of classes. The metavariables C and D, possibly with subscripts, range over class names. 7. OO: Syntax, where syntax occurring only at runtime appears shaded .

Each class has a name, a list of fields of the form t f, where f represents the field name and t its type, and a list of sessions of the form t η s { e }, where t is the return type, η the session descriptor, s the session name, and e the session body. For the sake of conciseness the symbol represents class extension, as in [START_REF] Igarashi | Featherweight Java: a Minimal Core Calculus for Java and GJ[END_REF]. All classes are defined as extensions of the topmost class Object.

Expressions include variables, that are both standard term variables x and the special variables this. The variable this is considered implicitly bound in any session declaration.

In a session request e.s {e : η} we call the expression e the cobody of the request (since it will be evaluated concurrently with the body of requested session). The session descriptor η represents the communications offered by the expression e .

In the session delegation expression, e • s {k : χ}, the filter χ represents the communication requirements in the choice of the session body and the channel k is added by the operational semantics in order to keep track of the channel to pass to the delegated session.

Channels are implicit in the source language syntax. At runtime, a pair of dual communication channels are introduced at each new session request.

The body of a communication expression is a pair of alternatives {t1 ⇒ e1 t2 ⇒ e2}, whose choice depends on the class of the object that is sent or received.

A runtime expression is either a user expression (i.e. an expression in Table 7 without shaded syntax) or an expression containing channels and/or object indentifiers. Furthermore, threads of runtime expressions can occur at runtime (see the operational semantics). Parallel threads are ranged over by P . Fully evaluated objects will be represented by object identifiers denoted by o.

Auxiliary Functions

As in FJ, a class table CT is a mapping from class names to class declarations with domain D(CT). Then a program is a pair (CT, e) of a class table (containing all the class definitions of the program) and an expression e (an expression belonging to the source language representing the program's main entry point). The class Object has no fields and its declaration does not appear in CT. As in FJ, from any CT we can read off the subtype relation between classes, as the transitive closure of clause. We assume a fixed CT. Thus, in the following, instead of writing CT(C) = class . . . we will simply write class C . . .. The class table CT satisfies some usual sanity conditions as in FJ [START_REF] Igarashi | Featherweight Java: a Minimal Core Calculus for Java and GJ[END_REF], but we allow the same session name to be declared with different session descriptors in a class hierarchy.

The fields lookup function is as in FJ. As for field type lookup we distinguish between the contexts where the field is used for reading (ftype r ) from those where it is for writing (ftype w ).

The stype lookup function returns a set of sets of session descriptors; in case it is invoked with a class name as argument, it will return a singleton containing a set of session descriptors. In this way we take into account the overloading and the fact that in general the type of the receiver is a boolean combination of classes.

The rtype and the sbody lookup functions take as arguments also a session descriptor: they return the return type of a session and the body of a session, respectively.

All these functions are defined in Table 8, where we define

m(f, a, t1, t2) = 8 > < > : f (a, t1) if t1 ≤ t2, f (a, t2) if t2 ≤ t1, ⊥ otherwise. .

Operational Semantics

Session invocation involves the creation of concurrent and communicating threads. These threads communicate by means of a pair of dual communication channels.

Objects passed in asynchronous communications are stored in a heap. A heap h is a finite mapping with domain consisting of objects and channel names. Its syntax is given by:

h ::= [ ] | o → (C, f : o) | k → o | h :: h
where::denotes heap concatenation.

The operational semantics associates to k and k two different queues of messages in the heap; when a thread, which uses the channel k, wants to receive a message it will inspect the queue associated to k, while, when it sends a message it will add it to the queue associated to k. Heap membership for object identifiers and channels is checked using standard set notation, by identifying h with its domain, we can also write o ∈ h, and k ∈ h.

The values that can result from normal termination are parallel threads of fully evaluated objects.

In the reduction rules we make use of the special channel addition operation ... defined in Table 9. We denote by e k the source expression e in which all occurrences of receive, send, and delegation expressions which are not within the cobody of a session request are extended, so that they explicitly mention the channel k they will use (remember that channel names are not written by the programmer).

The reduction is a relation between pairs of threads and heaps:

P, h -→ P , h
Reduction rules use evaluation contexts (based on runtime syntax) that capture the notion of the "next subexpression to be reduced":

E ::= [-] | E ; e | E .f | E .f := e | o.f := E | E .s {e : η} | E • s {k : χ} | k.sendC(E ){t1 ⇒ e1 t2 ⇒ e2}
The explicit mention of the evaluation context is needed in rule SESSREQ-R (Table 10), in which a new thread is generated in parallel with the evaluation context.

Reduction rules are in Table 10. Rule PAR-R models the execution of parallel threads. In this rule parallel composition is considered modulo structural equivalence. As usual, we define structural The successive four rules define the execution of standard objectoriented constructions.

e k = 8 > > > > > > > > > > > < > > > > > > > > > > > : e1 k ;e2 k if e = e1;e2, e1 k .f if e = e1.f, e1 k .f:=e2 k if e = e1.f:=e2, e1 k .s {e2 : η} if e = e1.s {e2 : η}, e1 k •s {k : χ} if e = e1•s {χ}, k.sendC(e0 k ){C ⇒ e k } if e = sendC(e0){C ⇒ e}, k.recC(x){C ⇒ e k } if e = recC(x){C ⇒ e}, e otherwise.
Rule SESSREQ-R models the connection between the cobody e of a session request o.s {e : η} and the body e of the session s, in the class of the object o, under the condition that e and e have dual session descriptors. This connection is established through a pair of fresh channels k, k. For this purpose the expression o.s {e : η} reduces, in the same context, to its own cobody e k and in parallel, outside the context, it spawns the body [ o /this]e k of the called session. The explicit substitution of k in e and of k in e ensures that the communication is on the fresh dual channels k and k. Thus, an object can serve any number of session requests.

Rule SESSDEL-R replaces the session delegation o • s {k : χ} by [ o /this]e k , where e is a body of the session s, in the class of the object o, such that the session descriptor of e is bigger or equal to the filter required by the delegation constructor. A part of the communication is delegated via the channel k to the object o: this delegation is transparent for the thread using the dual channel k. When the delegated job is over, the original thread can resume the communication via the channel k.

The communication rule for sendC, SENDCASE-R, puts the object o, i.e. the result of evaluating the expression e, in the queue associated to the dual channel k of the communication channel k. The computation then proceeds with the expression ei, if h(o) = (C, ) and C ≤ ti. Clearly if C ≤ t1 and C ≤ t2, the choice between e1 and e2 is non-deterministic, but we could choose some policy in order to have a deterministic choice, as done in [START_REF] Capecchi | Amalgamating Sessions and Methods in Object Oriented Languages with Generics[END_REF], [START_REF] Bettini | Session and Union Types for Object Oriented Programming[END_REF]. Dually the receive communication rule takes an object o from the queue associated to channel k and returns the expression [o/x]ei, if h(o) = (C, ) and C ≤ ti.

Typing

The presence in our calculus of the sequencing operator and of other operators which implicitly put in sequence the evaluation of expressions makes useful the definition of a concatenation operator ( • ) between session descriptors and the addition of the neutral element with respect to concatenation (ε). Instead we do not need the explicit session terminator end, so to sum up we have the

14 2009/1/21 fields(Object) = • fields(D) = t f class C D { t f; S } fields(C) = t f, t f fields(C) = t f ftype w (fi, C) = ftype r (fi, C) = ti ftype w (f, t1 ∧ t2) = m(ftype w , f, t1, t2) ftype r (f, t1 ∧ t2) = m(ftype r , f, t1, t2) ftype w (f, t1 ∨ t2) = 8 > < > : ftype w (f, t1) if ftype w (f, t1) ≤ ftype w (f, t2), ftype w (f, t2) if ftype w (f, t2) ≤ ftype w (f, t1), ⊥ otherwise. ftype r (f, t1 ∨ t2) = ftype r (f, t1) ∨ ftype r (f, t2) ftype w (f, ¬t) = ftype r (f, ¬t) = ⊥ class C D { t f; S } t η s { e } ∈ S stype(s, D) = {{η }} stype(s, C) = {{η, η }} class C D { t f; S } s ∈ S stype(s, C) = stype(s, D) stype(s, t1 ∧ t2) = m(stype, s, t1, t2) stype(s, t1 ∨ t2) = stype(s, t1) ∪ stype(s, t2) stype(s, ¬t) = ⊥ class C D { t f; S } t η s { e } ∈ S rtype(s, η, C) = t class C D { t f; S } t η s { e } ∈ S rtype(s, η, C) = rtype(s, η, D) rtype(s, η, t1 ∧ t2) = m(rtype, s, η, t1, t2) rtype(s, η, t1 ∨ t2) = rtype(s, η, t1) ∨ rtype(s, η, t2) rtype(s, η, ¬t) = ⊥ class C D { t f; S } t η s { e } ∈ S sbody(s, η, C) = e class C D { t f; S } s ∈ S sbody(s, η, C) = sbody(s, η, D) Table 8. OO: Lookup Functions. PAR-R e, h -→ P, h e || P1, h -→ P || P1, h SEQ-R E [o; e], h -→ E [e], h FLD-R h(o) = (C, f : o) E [o.fi], h -→ E [oi], h NEWC-R fields(C) = t f o ∈ h E [new C(o)], h -→ E [o], h :: [o → (C, f : o)] FLDASS-R E [o.f := o ], h -→ E [o ], h[o → h(o)[f → o ]] SESSREQ-R h(o) = (C, ) η η sbody(s, η , C) = e k, k ∈ h E [o.s {e : η}], h -→ E [e k ] || [ o /this]e k , h[k, k → ()] SESSDEL-R h(o) = (C, ) χ ≤ η sbody(s, η, C) = e E [o • s {k : χ}], h -→ E [[ o /this]e k ], h SENDCASE-R h( k) = o h(o) = (C, ) C ≤ ti E [k.sendC(o){t1 ⇒ e1 t2 ⇒ e2}], h -→ E [ei], h[ k → o :: o] RECEIVECASE-R h(k) = o :: o h(o) = (C, ) C ≤ ti E [k.recC(x){t1 ⇒ e1 t2 ⇒ e2}], h -→ E [[ o /x]ei], h[k → o]
Table 10. OO: Reduction Rules.

following syntax for session descriptors:

η ::= ε | !t.η ⊕ !t.η | ?t.η + ?t.η
and we define:

η • η = ( η if η = ε, α.(η • η ) if η = α.η
where α ∈ {!t, ?t}. The descriptor ε is dual of itself.

We first define typing for user expressions, in which communication channels are implicit. For technical reasons it is useful to consider also expressions with occurrences of object identifiers, which are not directly expressible in user syntax. We call these expressions channel free expressions. The term environments there-fore will contain also type assignments to object identifiers. This permits a simpler formulation of the runtime typing rules.

The typing judgement has the shape

Γ e : t η
where Γ is a term environment, which maps this, variables and objects to types, and η represents the session descriptor of the (implicit) active channel. Typing rules for channel free expressions are in Table 11. For the sake of simplicity in rule NEWC-T we require that the initialisation of an object does not involve communications. Notice that in rule SEQ-T we use concatenation to represent that first the communications in e1 and then those in e2 are performed.

RECEIVEC-RT

Γ , x : ti r ei : t {k : ηi} Γ r k.recC(x){t1 ⇒ e1 t2 ⇒ e2} : t {k : ?t1.η1 + ?t2.η2} Table 13. OO: Typing Rules for Runtime Expressions.

The rule for session request SESSREQ-T prescribes that in all sets of session descriptors which build stype(s, t) there is a session descriptor which is dual of the session descriptor of the the cobody e . This assures that there is always a possible choice for the body of the session s which will communicate properly with the cobody. In typing session delegation (rule SESSDEL-T) we take into account that the whole expression will be replaced by one of the session bodies defined in the class of the expression to which the session is delegated (cf. the reduction rule SESSDEL-R, Table 10). The condition χ ≤ η implies rtype(s, η , t) = t assures that all bodies of s which can be chosen have the same return type.

Table 12 defines well-formed class tables. Rule SESS-WF type checks the session bodies with respect to the current class C taking as term environment the association between this and C.

During evaluation of well-typed programs, channel names are made explicit in send and receive expressions, as well as in session delegation. Thus, in order to show how well-typedness is preserved under evaluation, we need to define new typing rules for runtime expressions. Furthermore, in typing runtime expressions, we must take into account the session types of more than one channel: runtime expressions contain explicit channel names (used for communication) thus session types must be associated with channel names in an appropriate way. Then judgements have the form Γ r e : t Θ where Θ denotes a session environment which maps channels to session descriptors.

A session environment maps only a finite set of channels to session descriptors different from ε, and all the remaining to ε. We can then represent one session environment with an infinite number of finite sets which give all the meaningful associations and some of the others. For example {k : η} and {k : η, k : ε} represent the same environment. This choice avoids an explicit weakening rule for session environments. Table 13 gives the typing rules for runtime expressions, which differ from those for channel free expressions for having session environments instead of a unique session descriptor. For this reason we extend the concatenation of session descriptors to session environments as follows:

Θ • Θ (k) = Θ(k) • Θ (k).
Notice that in rule SESSREQ-RT we are making use of the judgement Γ e : t η , where the expression e does not contain channels, but it can contain object identifiers. This justifies our choice of considering channel free expressions instead of user expressions in the typing rules of previous subsection. Notice also that the session environments of the branches in the communication expressions only contain the current channel as subject, since these expressions will never be reduced before the selection has been done.

Our type system enjoys subject reduction and assures progress (-→ * is the reflexive and transitive closure or -→): THEOREM 3.7 (Subject Reduction and Progress). If ∅ e0 : t0 ε and e0, [ ] -→ * P, h, where P ≡ e1 || . . . || en, then:

1. for each ei we get Γ r ei : ti Θi for some Γ , ti, Θi (1 ≤ i ≤ n), and there is j (1 ≤ j ≤ n) such that tj = t0, and; 2. either P, h -→ P , h for some P , h , or for all i (1

≤ i ≤ n)
ei is an object identifier.

The proof of this theorem is the content of Appendix C. Notice that evaluation of closed expressions stops returning a parallel of object identifiers and that an object identifier can be typed, using the type system for channel free expressions, from the context Γ which defines the type assumption for that identifier.

The runtime errors which our type system prevents are:

1. the selection of a field and the request of a session which do not belong to the class of the current object;

2. the creation of a pair of dual channels whose communication sequences do not perfectly match.

Conclusions and related work

We have defined a semantic theory of session types by subverting the usual session type presentations, where the subtyping (and subsession) relations are introduced first, and then shown to be sound. Here we have focused on duality as the main characterizing feature, and defined subtyping and subsessioning in terms of it. We claim that our theory of session types is minimal-insofar as the addition of any further constructor such as parallel composition or labeled synchronization would restrict the programming language to which the framework could be applied-and yet complete. The key ingredients of our theory are communication primitives, behavioral composition operators for describing branching points, and boolean composition operators for types and sieves. All the existing proposal of session types of comparable expressiveness can be obtained by using suitable combinations of these ingredients and our session types can be used for typing generic π-calculus processes without any dedicated primitive for session management.

The relation of our work with some others defining theories of session types is already explored in Section 3. Subtyping relations for session types are studied in [START_REF] Gay | Subtyping for session types in the pi-calculus[END_REF][START_REF] Gay | Bounded polymorphism in session types[END_REF]. In these works the definition of the subtyping relation is driven by the observation that one can safely replace a session by another that externally offers more choices and internally can make less choices. Since in the cited works choices are guarded by labels, it turns out that external and internal choices have the same subtyping relation as record and variant types respectively. Here we work with external choices that are driven by the messages being exchanged rather than by labels: when a session offers an output it will be able to synchronize only with the branches of a choice that accept that output. This policy was first considered in [START_REF] Dezani-Ciancaglini | Bounded session types for object-oriented languages[END_REF] for an object-oriented calculus. The resulting subtyping relation generalizes the safe substitutability principle of the existing settings by permitting (a combination of) branches of a choice to subsume another set of branches. Furthermore, while in the cited works the subtyping relation is defined coinductively and axiomatically, we characterize the relation semantically, and this captures directly the desired safety property.

Our approach to session type semantics is akin to the testing approach to process semantics [START_REF] De Nicola | Testing equivalences for processes[END_REF]: the notion of "passing a test" is embodied in our notion of duality, and subsessioning is the preorder induced by comparing the duals of two session types. In particular, two session types are equivalent if they have the same set of duals. Unlike the standard testing theories, our notion of duality is symmetric (in the spirit of the session types literature).

Moving from label-driven to type-driven branch selection may seem a regression, insofar as it demands run-time type checking. This is not so in practice. First, when sessions are used as in any of the existing session types proposals, branching can be easily optimized by reducing run-time type checking to label/class matching. Second, general value-based dispatching can be implemented very efficiently anyway [START_REF] Frisch | Regular tree language recognition with static information[END_REF], with the exception of session type values which may require to check subsessioning. In any case, it is reasonable to assume that the matching overhead is negligible with respect to latency time of communications typical of service-oriented computing.

With respect to concurrency theory we introduce an original treatment of output signals, by implementing a form of partial asynchrony. This treatment is similar to the one proposed by Castellani and Hennessy [START_REF] Castellani | Testing theories for asynchronous languages[END_REF] for asynchronous CCS, where outputs cannot be blocked even if they guard external choices (we called this property "output irrevocability"). However, in our setting output signals are allowed to have a continuation. Thus the order of actions specified by a session type must be strictly followed (equivalence of session types modulo permutation of consecutive outputs is left for future work). Technically, this corresponds to observing inputs even in the presence of (partial) asynchrony.

From a technical viewpoint in this work we introduce several novelties. We devise a new labeled transition system for session descriptors in which actions represent values rather than types, we give a semantic characterization of the subsessioning relation in terms of a set-theoretic interpretation of session descriptors. The same interpretation is used to give semantics to a complete set of Boolean operators for session descriptors. A labeled transition system for session types is also proposed in [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF], where a type system ensuring progress for the CaSPiS calculus [START_REF] Boreale | Sessions and pipelines for structured service programming[END_REF] is designed.

A. Proofs of Section 2

We will first prove Theorems 2.15 and 2.18 by simultaneous induction and then Proposition 2.10 and Theorem 2.12 since the latest two proofs use the strong normal forms of sieves. Notice that this does not introduce circularity since the first proof is independent from Proposition 2.10 and Theorem 2.12.

A.1 Proof of Theorems 2.15 and 2.18

We prove Theorems 2.15 and 2.18 by simultaneous induction. More precisely we consider the weight defined in the proof of Theorem 2.6. Then we prove:

1. Each sieve χ can be effectively transformed into an equivalent strong normal form whose weight is smaller than or equal to the weight of χ.

2. χ ≤ χ is decidable.

First of all notice that by classical set theoretic transformations it is possible to put every sieve in disjunctive normal form. This can be effectively done by the regularity of the trees. So let us assume that all the sieves we use in this proof are in disjunctive normal form.

Base case. The base case for weight 0 is when both χ and χ are possibly empty sums of end's. The normal form of all such sieves is end (which can be obtained by rules (E1) and (I1) of Table 1) and χ ≤ χ is easily decidable.

Inductive case.

Let us now study the inductive case, and therefore suppose the two properties hold for sieves of strictly smaller weight. For the sake of the presentation we prove the two points one after the other, although we should do the proof of the two properties-in this order-for each case.

Thus let us start proving the point 1 by performing a case analysis on the form of χ.

If χ ≡ W i∈I V j∈J λij where |I| > 1, then we have to discard all the intersections that are bottom, that is all V j∈J λij = ⊥. Whether each of these intersections is equivalent to bottom can be effectively decided by induction hypothesis thanks to the point 2 of the theorem. The normal form is then obtained by coinductively applying the transformation on all remaining literals, which is possible thanks to the induction hypothesis.

If χ ≡ V j∈J λj where at least one literal is not negated. The normal form is either ⊥, or it is obtained by a coinductive application of the transformation. The latter is always possible thanks to the induction hypothesis. Thus all it remains to prove is that we can decide whether χ is ⊥. Since we cannot directly use the induction hypothesis (as we should apply it to the whole sieve),

[R-EX-SPLIT] X i∈I ?ψi.ηi{ + end} ≤ X j∈J\{k} ?ψ j .η j + ?(ψ k \ ψ h ).η k + ?ψ h .η k { + end} X i∈I ?ψi.ηi{ + end} ≤ X j∈J ?ψ j .η j { + end} " ψ h ψ k ψ h = ψ k « [L-EX-SPLIT] X i∈I\{h} ?ψi.ηi + ?(ψ h \ ψ k ).η h + ?ψ k .η h { + end} ≤ X j∈J ?ψ j .η j { + end} X i∈I ?ψi.ηi{ + end} ≤ X j∈J ?ψ j .η j { + end} " ψ k ψ h ψ h = ψ k « [LR-EX-SPLIT] X i∈I\{h} ?ψi.ηi + ?(ψ h \ ψ k ).η h + ?ψ k .η h { + end} ≤ X j∈J\{k} ?ψ j .η j + ?(ψ k \ ψ h ).η k + ?ψ h .η k { + end} X i∈I ?ψi.ηi{ + end} ≤ X j∈J ?ψ j .η j { + end} 0 @ ψ k ∧ψ h = ∅ ψ k ∧ψ h = ψ k ψ k ∧ψ h = ψ h 1 A [R-IN-SPLIT] M i∈I !ψi.ηi{ ⊕ end} ≤ M j∈J\{k} !ψ j .η j ⊕ !(ψ k \ ψ h ).η k ⊕ !ψ h .η k { ⊕ end} M i∈I !ψi.ηi{ ⊕ end} ≤ M j∈J !ψ j .η j { ⊕ end} " ψ h ψ k ψ h = ψ k « [L-IN-SPLIT] M i∈I\{h} !ψi.ηi ⊕ !(ψ h \ ψ k ).η h ⊕ !ψ k .η h { ⊕ end} ≤ M j∈J !ψ j .η j { ⊕ end} M i∈I !ψi.ηi{ ⊕ end} ≤ M j∈J !ψ j .η j { ⊕ end} " ψ k ψ h ψ h = ψ k « [LR-IN-SPLIT] M i∈I\{h} !ψi.ηi ⊕ !(ψ h \ ψ k ).η h ⊕ !ψ k .η h { ⊕ end} ≤ M j∈J\{k} !ψ j .η j ⊕ !(ψ k \ ψ h ).η k ⊕ !ψ h .η k { ⊕ end} M i∈I !ψi.ηi{ ⊕ end} ≤ M j∈J !ψ j .η j { ⊕ end} 0 @ ψ k ∧ψ h = ∅ ψ k ∧ψ h = ψ k ψ k ∧ψ h = ψ h 1 A
Table 14. Algorithmic subsessioning simplification rules. In these rules we use to denote either ≤ or <:, curly braces to denote optional end summands, and suppose that all operators are uniformly applied either on types or on sieves.

let us separate negated literals from positive ones. That is, define

J = P ∪ N , such that χ ≡ V p∈P ηp ∧ V n∈N ¬ηn. Then χ ≤ ⊥ if and only if L p∈P ηp ≤ W n∈N ηn, if

and only if-by the strong disjunction property for descriptors-

L p∈P ηp ≤ ηn holds for all n ∈ N . This can be decided by induction hypothesis using the point 2 of the theorem.

If χ ≡ V j∈J ¬ηj. As above, let us first show that it is possible to decide that χ ≤ ⊥, that is whether ¬ W j∈J ηj ≤ ⊥. This is always true for Lemma 2.16, therefore we can coinductively apply the transformation by induction hypothesis.

All the coinductive transformations above terminate by the regularity of our sieves. Furthermore it is easy to see that they do not increase the weight of the sieves.

If χ ≡ η, and the descriptor is prefixed then we check that its prefix is not ∅ (which can be done by induction hypothesis) and possibly coinductively apply the transformation on its continuation.

Otherwise we will do the following transformations:

1. get rid of every subterm of the form ?ψ.η and !ψ.η such that ψ = ∅ by means of rules (B1), (B2), (E8), and (I8);

2. get internal choices of external choices of prefixed descriptors and end using (E4);

get internal choices of:

• external choices of input descriptors and possibly of end

• output descriptors

• possibly end by applying the rules (O1), (O2), and (O3) inside the external choices. I.e. we obtain a descriptor of the shape:

M J∈K ( X j∈J ?ψj.ηj{ + end}) ⊕ M h∈H !ψ h .η h { ⊕ end} (12)
4. we have the following cases:

(a) K = ∅.

(b) H = ∅. Then ( 12) is equivalent to: where K = {J1, . . . , J k } and ψj 1 ∧ • • • ∧ ψj k = ∅ and end is present only if it occurs in all the external choices of ( 12).

X j 1 ∈J 1 • • • X j k ∈J k ?(ψj 1 ∧ • • • ∧ ψj k ).(ηj 1 ⊕• • •⊕ηj k ){+end} (13)
(c) K, H = ∅ and end is present in all external choices. Then ( 12) is equivalent to

η = M h∈H !ψ h .η h ⊕ end (14)
(d) K, H = ∅, at least one external choice has no end subterm. Then ( 12) is equivalent to ⊥.

5. in cases (4a) and (4c) we can obtain an internal choice of outputs and possibly end such that if !ψ and !ψ are two top level prefixes we have ψ ∧ ψ = ∅ by applying rules (O4), (O5), and (I5).

6. in case (4b) we obtain an external choice of inputs and possibly end such that if ?ψ and ?ψ are two top level prefixes we have ψ ∧ ψ = ∅ by applying rules (E5), (E6), and (E7).

7. we convert any χ occurring in a top level prefix in strong normal form (this can be effectively done by the induction hypothesis).

8. we coinductively apply the algorithm to every continuation of every top level guarded descriptor of the (internal or external) choice.

Note that the coinductive application of the algorithm terminates by the regularity of our descriptors. All it remains to prove is that the passage from step (3.) to step (4.) is is sound, that is it yields an equivalent descriptor.

For case (4a) this is trivial.

For case (4b) we have that equation ( 12) becomes an internal choice of external choices of inputs. Let us examine the set of duals of [START_REF] De Nicola | CCS without τ 's[END_REF]. Since we only have inputs then we have to check which inputs are guaranteed. These are exactly all the inputs that are guaranteed by all the summands of the internal choice, that is those that are emitted by all prefixes, and thus by their intersection. The continuation of this intersection is then obtained by the definition of successor yielding the descriptor [START_REF] Dezani-Ciancaglini | Bounded session types for object-oriented languages[END_REF].

In case (4c) by the irrevocability of outputs we have to check which outputs are offered in order to characterise the set of duals of [START_REF] De Nicola | CCS without τ 's[END_REF]. It is easy to see that ( 12) and ( 14) offer the same outputs and they both offer end.

In case (4d) [START_REF] De Nicola | CCS without τ 's[END_REF] is not viable since it does not converge and therefore it is equivalent to ⊥.

Let us pass to the proof of point 2, that is show that it is possible to decide whether χ ≤ χ holds. Thanks to point 1 we can suppose that both χ and χ are in strong normal form.

We proceed by case analysis on the form of χ and χ by starting with the simplest cases first.

Case

W i∈I V j∈J λij ≤ W h∈H V k∈K λ hk such that |I| > 1.
We can split the union on the left, and reduce this problem to check whether there exists i ∈ I such that

V j∈J λij ≤ W h∈H V k∈K λ hk ,
V p∈P J θp ∧ V n∈N J ¬ηn ≤ V p∈P K θp ∧ V n∈N K ¬ηn. By simple set-theoretic manipulations this is equivalent to check whether V p∈P J ∪P K θp ≤ W n∈N J ∪N K ηn.
Since intersection is equivalent to internal choice this is reduced to checking whether L p∈P J ∪P K θp ≤ W n∈N J ∪N K ηn which by strong disjunction is equivalent to prove that L p∈P J ∪P K θp ≤ ηn holds for all n ∈ NJ ∪ NK . The result follows by induction hypothesis.

Case η ≤ η . This is the last remaining case and also the most difficult one. We can feed η and η to the algorithmic rules of Table 2. So to prove this case we have to prove that these rules are sound and complete with respect to the semantic definition of subtyping.

Soundness. For soundness, let us prove the point by induction on the Noetherian measure defined in Section 2.1. More precisely for each rule of Tables 2 and14 we must prove that the set of duals of the lhs of its conclusion is included in the set of duals of the rhs. Let us proceed by a case analysis on the last rule applied in the deduction of η ≤ η .

Case [END] and [MIX-CHOICES]. The result follows by a direct application of the definition of duality.

Case [EXT-CHOICES]. By induction hypothesis for all i ∈ I the set of duals of ηi is contained in the set of duals of η i . We have two subcases. (i) Case |I| > 1: since both descriptors are in strong normal form, then they can only emit input signals or a tick; thus for these choices we can apply only the rules TR3 and TR4; this implies that the signals emitted by each descriptor in the conclusion are exactly the same as those of their subcomponents. The result follows by the definition of duality. (ii) Case |I| = 1: then there are three subcases. Either the lhs of the conclusion emits an input, and then we proceed as in the case before; or it is an end, but then one of the summands of the rhs is also end, and the result follows from the definition of duality as both must ensure ; or it is of the form !ψ.η , but then also |J| = 1 and therefore this rule does not apply ([PREFIX] should be used instead).

Case [INT-CHOICES]. Similar to the previous case. Case [*-SPLIT] Notice that by rules I5-I7 and E5-E7 the corresponding session descriptors at the premise and at the conclusion of each rule have exactly the same set of duals, whence the result.

Case [PREFIX]. This is the hard case since we cannot use the induction hypothesis as the Noetherian measure may increase. We are in the case where we have deduced α.θ ≤ α.θ from θ ≤ θ . So let us consider the deduction for θ ≤ θ and explore it upwards from the root. By the regularity of our descriptors we have just two possible cases: either we traverse a finite (and possibly null) number of applications of the PREFIX rule and arrive to the application of a different rule, or we traverse an again finite (and possibly null) number of applications of the PREFIX rule and arrive to the judgment θ ≤ θ . The latter case is straightforward because it means that θ ≡ θ , therefore the result holds for reflexivity. In the former case instead we perform a case analysis on the rule we have reached, apply the same reasoning as above for the corresponding case and deduce the result by Lemma 2.17.

Completeness. For completeness let us prove this point by induction on the Noetherian measure defined in Section 2.1. Suppose that the result holds for descriptors of smaller measure and let us prove for the general case. Imagine by contradiction that the result does not hold for the general case. Then there exist η and η such that all the duals of η are also duals of η but for which the algorithm answers no. Therefore there exists at least one rule that fails. Since we did not put any constraint on η and η , then we can consider without loss of generality that it is the last one and that all the preceding applications of the rules hold. Let us then perform a case analysis on this rule:

Case [END]. This is the base case and vacuously holds since it cannot fail.

Case [PREFIX]. This is another base case and vacuously holds since it cannot fail (if it fails it is because the premise failed, but this contradicts the fact that the PREFIX rule is the last one to have failed).

Case [MIX-CHOICES]. The last base case. It may have failed because one (or both) of the two end's is absent, but this contradicts our hypothesis: if it is the rhs end that is missing then end is a dual of the first but not of the second; if it is the lhs end that is missing then I is not empty (otherwise the rule would not fail), but then since the types are in strong normal form a dual of ηi cannot be dual of the lhs, since both of them ensure an input. It may have also failed because the internal choice is on the right and the external one is on the left (strictly speaking this is not a failure of this rule but it is the only case in which no rule applies), but then it is easy to build a dual for the lhs which is not dual for the rhs.

Case [EXT-CHOICES]. If this failed it is because there exists i ∈ I such that for all j ∈ J, ηi ≤ ηj. By induction hypothesis since the algorithm is complete, then there exists θ that is dual of ηi but it is not dual of any ηj. Assume η ≡ P i∈I ?ψi.ηi{ + end}, where the end subterm may be missing. Then η must be justified by condition (1) of Definition 2.9, namely there exists µ such that η ⇓ µ and η µ . If µ = , then we conclude immediately by taking η = end. If µ = , then there exists k ∈ I such that ?ψ k .η k ⇓ µ and η µ . Because η is in disjoint normal form we have ?ψi.ηi ⇓ µ implies η µ = ηi for every µ . Hence we conclude by taking η = !ψ k .η k .

Assume η ≡ L i∈I !ψi.ηi{ ⊕ end}, where the end subterm may be missing. Then η must be justified by condition (2) of Definition 2.9, namely for every i ∈ I we have !ψi.ηi ↓ µ for some µ and η i since η µ = ηi. We conclude by taking η = P i∈I ?ψi.ηi + end. The proof that η η is trivial. (⇐) It is sufficient to show that the relation R = {η | ∃η : η η } is a coinductive viability. Let η ∈ R. Then there exists η such that η η . We reason by cases on the justification of η η according to Definition 2.5.

Assume η η is justified by condition (1) of Definition 2.5. Then η ⇓ and η ⇓ . Hence condition (2) of Definition 2.9 is satisfied (note that end ∈ R by definition of R).

Assume η η is justified by condition (2) of Definition 2.5. Then η ↓ and η ↓ µ implies η ⇓ µ and η µ η µ . By definition of R we have η µ ∈ R, hence condition (1) of Definition 2.9 is satisfied.

A.3 Proof of Theorem 2.12 (⇒) Assume η1 η2 and η 1 . By Proposition 2.10 we have that η1 is viable. Let η η1. It is sufficient to show that for otherwise end η and end η which is absurd by definition of R. If µ = , then there exists i ∈ I such that ?ψi.ηi ⇓ µ and η i . Suppose by contradiction that η ⇓ µ and consider θ ≡ !ψi.θi where θi is an arbitrary dual of ηi (it exists from the hypothesis η i and by Proposition 2.10). Then θ η but θ η which is absurd. Hence there exists j ∈ J such that ?ψj.ηj ⇓ µ. By definition of duality we deduce θi ηi and θi ηj, hence (ηi, ηj) ∈ R since θi is arbitrary. We conclude by observing that η µ = ηi and η µ = ηj. Condition (3) of Definition 2.11 is trivially satisfied since η ⇓.

C = {(η , η 2 ) | ∃η 1 : η η 1 ∧ η 1 η 2 } is a
Assume η ≡ L i∈I !ψi.ηi{ ⊕ end} and η ≡ L j∈J !ψj.ηj{ ⊕ end} and η ⇓. As regards condition (1) of Definition 2.11, for every i ∈ I let θi be an arbitrary session descriptor such that θi ηi (these descriptors exist because η ). Let θ ≡ P i∈I ?ψi.θi{ + end} where the end subterm is present only if it is present also in η. Assume η ↓ µ. Then there exists j ∈ J such that !ψj.ηj ↓ µ. Suppose contradiction that η ↓ µ. Then θ η but θ η , which is absurd. Hence there exists i ∈ I such that !ψi.ηi ↓ µ. We derive (ηi, ηj) ∈ R since θi is arbitrary. We conclude by observing that η µ = ηi and η µ = ηj. Condition [START_REF] Bonelli | [END_REF] The partial order relation between session stacks and session environments takes into account their evolution due to process and system reductions. It is easy to verify that agrees with the mapping set and with union of session environments.

PROPOSITION B.5. 1. If ∆ ∆ , then set(∆) set(∆ ). 2. If Λ1 Λ 1 and Λ2 Λ 2 , then Λ1 ∪ Λ2 Λ 1 ∪ Λ 2 .
As usual generation and substitution lemmas are the key of our subject reduction proof.

LEMMA B.6 (Generation Lemma for Processes

P : (h : η • x : η ) and χ ≤ η . 7. If Γ h!h P : ∆, then core(∆) = (h : !χ.η • (h : η • ∆ )) and Γ P : (h : η • ∆ ) and η ≤ χ. 8. If Γ P + Q : ∆, then core(∆) = (h : η1 + η2 • ∆ ) and Γ P : (h : η1 • ∆ ) and Γ Q : (h : η2 • ∆ ). 9. If Γ P ⊕ Q : ∆, then either core(∆) = (h : η1 ⊕ η2 • ∆ )
and Γ P : (h : η1 • ∆ ) and Γ Q : ∆ , h : η2 or Γ P : ∆, and Γ Q : ∆.

LEMMA B.7 (Generation Lemma for Systems). 1. If Γ P : Λ, then there exists ∆ such that Λ = set(∆) and Γ P : ∆.

If Γ

S T : Λ, then there exist Λ1 and Λ2 such that Λ = Λ1 ∪ Λ2 and Γ S : Λ1 and Γ T : Λ2.

LEMMA B.8 (Substitution

). 1. If Γ , x : t S : Λ and v : t, then Γ S[ v /x] : Λ. 2. If Γ S : Λ, x : η, then Γ S[ k /x] : Λ, k : η.
The following lemma relates the one step reductions of processes with labels different from τ with the changes of the session stacks. LEMMA B.9. Let Γ P : ∆, then 1. If P c t !(x:η) -→ P , then Γ P : (x : η • ∆). We can show that starting from an initial system we only get coherent session environments, i.e., session environments in which dual internal channel are mapped to dual session descriptors. 1. dom(core(∆i)) only contain internal channels; 2. no dom(core(∆i)) contains an internal channel and its dual; 3. S 1≤i≤n set(core(∆i)) and Σ are coherent.

DEFINITION B.14 (Coherent session environment

PROOF. By induction on

τ =⇒ using Lemmas B.9 and B.10. If S is an initial system, then it is a parallel composition of sums of ![z]. Then S satisfies banally the three conditions above.

Let S be the system obtained from S after a finite sequence of reductions, in which the three conditions above hold, and S can still perform a τ action. If we can apply rule CONNECTION we get a system which still satisfies the conditions because this rules pushes in both session environments the assumptions k : η and k : η , for some fresh k and with η η . If we can apply rules COMMUNICATION or DELEGATION we get a system which still satisfies the conditions because the successors of dual sessions are still dual sessions by definition of duality.

We restate here Lemma 3.5 by taking advantage of the definition of core. Indeed S : Λ with S closed implies that the set of internal channels which occur in S is the domain of core(Λ).

PROOF. By induction and by cases on

τ =⇒. The more interesting case is that of rule DELEGATION with S T : Λ and:

Σ S k! k 1 -→ Σ S Σ T k? z:χ -→ Σ T Σ(k1) ≤ χ Σ, k : η, k : η S T τ -→ Σ S T [ k 1/ z] where Σ = Σ, k : η !Σ( k1) , k : η ?Σ( k1) . Note that Σ (k) = Σ(k) !Σ( k1) , Σ ( k) = Σ( k) ?Σ (
(k) = !χ .Λ (k) { +θ }, Λ( k) = ?χ.Λ ( k) { +θ}, χ ≤ Λ (k1) and Λ(k1) ≤ χ . By induction Σ(k) ≤ Λ(k), Σ( k) ≤ Λ( k)
, and Σ(k1) ≤ Λ(k1). We get Σ (k1) ≤ Λ (k1) from Σ (k1) = Σ(k1) ≤ χ ≤ Λ (k1). From Σ(k1) ≤ Λ(k1) and Λ(k1) ≤ χ and the coherence of Σ we derive that Σ( k1) is dual of χ and therefore Λ(k) !Σ( k1) ≤ Λ (k). From Σ(k) ≤ Λ(k) we have Σ(k) !Σ( k1) ≤ Λ(k) !Σ( k1) and so we conclude Σ (k) ≤ Λ (k). Similarly from Σ(k1) ≤ χ we derive that Σ( k1) is dual of χ and therefore Λ( k) ?Σ( k1) ≤ Λ ( k). From Σ( k) ≤ Λ( k) we have Σ( k) ?Σ( k1) ≤ Λ( k) ?Σ( k1) and so we conclude Σ ( k) ≤ Λ ( k).

The last technical tool we use is to index the internal channels with increasing indexes according to their order of creation. LEMMA B.16. If S is initial and S τ =⇒ Σ P1 . . . Pn, and the fresh internal channels take successive numbers according to the order of creation, then Γi Pi : ∆i implies that the indexes of internal channels in ∆i are decreasing for 1 ≤ i ≤ n.

PROOF. By induction on

τ =⇒ using Lemma B.9 and B.10. Notice that the only rule which adds channels to a possibly non empty stack is CONNECTION and this rule adds the internal channels with the maximum index. THEOREM 3.6 (Progress) Every initial system satisfies the progress property.

PROOF. Let S be initial and S τ =⇒ Σ P1 . . . Pn, where Pi : ∆i. It is easy to verify that P1 . . . Pn : Λ, where Λ = S 1≤i≤n set(core(∆i)). Assume the fresh internal channels take successive numbers according to the order of creation and j be the maximal index of the internal channel which occur in Λ. By Lemma B.15(2) there are l, l such that kj ∈ dom(core(∆ l )) and kj ∈ dom(core(∆ l )). By Lemma B.16, kj and kj must be the top of ∆ l and ∆ l , respectively. Note that by Lemma 3.5 Σ satisfies the conditions of Lemma B.12 for ∆ l and ∆ l . Therefore at least one of the following alternatives holds:

; h) if 1. h(o) = (C, f : o), ftype r (C, fi) = t ⇒ h(o)(fi) = (C , ), C <: t, 2. ∀o ∈ dom(Γ ), h(o) = (Γ (o), -).
In point 1 of the above definition, recall that ftype r (C, fi)=ftype w (C, fi) being C a class.

We type only single expressions, but they can result in parallel threads. Since we do not have a typing for parallel threads we require each single expression to be well-typed. Moreover we want to get our property in the most general form, allowing the property to hold for all well-typed expressions, which sometimes can be generated by initial expressions only in parallel with other expressions. For example, no initial expression can reduce to the expression Notice also that receive expressions can never get objects of wrong types. For example the execution of k.recC(x){Bool ⇒ ¬x} if h(k) = 3 is simply stopped, i.e. it does not produce a runtime error. For this reason, in contrast to the calculus of [START_REF] Coppo | Asynchronous Session Types and Progress for Object-Oriented Languages[END_REF], we do not need to require agreement between the objects in the queues associated to channels by the heap and the session types of the same channels in the session environment. The example above also suggests that this agreement will be a key ingredient of the progress proof.

The typing rules for runtime expressions differ from the ones for user expressions only in assigning the session type to explicit channels, not in the union type. The relations between the two systems are clarified by the following proposition that will be essential in considering the progress property. PROPOSITION C.3. Γ e : t η implies Γ r e k : t {k : η}. Let us notice that Γ r e : t ∅ is equivalent to Γ r e : t {k : ε} by our convention on session environments.

We now introduce some lemmas used in the proof of the Theorem C.1; their proofs are trivial and then are omitted.

Lemma C.4 states that every expression, different from an object, can be written as a composition of an evaluation context and a redex, where the set of redexes is defined by:

new C(o) | o.f | o.f := o | o.s {e : η} | o • s {k : χ} k.sendC(o){C ⇒ e C ⇒ e} | k.recC(x){C ⇒ e C ⇒ e}
The fact that the evaluation context is unique expresses the determinism of the evaluation strategy.

LEMMA C.4. Let e be a runtime expression such that:

1. e is not an object, 2. Γ r e : t Θ for some Γ , Θ and t, then there exists a unique evaluation context E such that e = E [r] for some redex r.

The following lemma states the obvious property that, in any type derivation ending by rule SUB-RT, there is a subderivation giving a subtype to the same expression such that its final rule is different from SUB-RT. LEMMA C.5. In any derivation of Γ r e : t Θ there is a subderivation of Γ r e : t Θ, with t <: t , where the last applied rule is different from SUB-RT. LEMMA C.6 (Subderivations). If Γ r E [e] : t Θ, then there exist Θ1, Θ2, t , such that for all x fresh in E , Γ , we get Θ = Θ1 • Θ2, and Γ r e : t Θ1, and Γ (x : t ) r E [x] : t Θ2.

Lemma C.7 allows the combination of the typing of E [x] and the typing of e, provided that the type of e is the same as that of x in the first typing.

LEMMA C.7 (Context Substitution). If Γ r e : t Θ1, and Γ (x :

t) r E [x] : t Θ2, then Γ r E [e] : t Θ1 • Θ2.
The following lemma expresses the weakening property for term environments.

LEMMA C.8 (Weakening). Let Γ r e : t Θ.

1. If x ∈ dom(Γ ) then Γ (x : t ) r e : t Θ. 2. If o ∈ dom(Γ ) then Γ (o : C) r e : t Θ.
As usual, for proving Subject Reduction, it is handy to show preservation of typing under term substitution. THEOREM (Subject Reduction). If wf(Γ ; h) and Γ r e : t Θ then 1. e, h -→ e , h implies that there exist Θ , Γ such that Γ ⊆ Γ and Θ Θ , and wf(Γ ; h ), and Γ r e : t Θ . 2. e, h -→ e1 || e2, h implies that h = h[k, k → ( )] for some fresh k, and wf(Γ ; h ), and that there exist t , η, η such that Γ r e1 : t Θ, {k : η}, and Γ r e2 : t { k : η }, and η η .

By induction on the definition of -→. We proceed by case analysis.

By Lemma C.5 we consider typing derivations of Γ r e : t Θ where the last applied rule is different from the rule SUBRT.

Let the last applied rule be SESSREQ-R: The remaining cases easily follow from the induction hypothesis.

C.2 Proof of Progress

The proof of progress requires to study global properties of type preservation during the reduction of parallel threads. Namely we need to take into account the objects in the queues associated to channels and their relations with the session types of the channels themselves. In the following definition we extend the notion of duality between session types taking into account also the objects already sent by a thread, and waiting to be read by the thread which has the dual channel. DEFINITION C.11. Let h be a heap, o be a queue of objects in h and η, η two session types. The relation η o h η is defined by: 1. η Intuitively, the definition above describes an agreement between the (session) type η of a channel k and the type η of k after the objects o have been memorized in the queue associated with k in h (recall that communication is asynchronous and that only one between the queues h(k) and h( k) can be nonempty). Thus, when the queue is empty (case (1) of the definition), η and η agree if they are dual. When the queue is o :: oi (case (2)), if the type η agrees with (!t1.η1 ⊕ !t2.η2) • η after the objects o have been put in the queue, then it also agrees with the type ηi • η , where ηi is the session type of the branch obtained after putting in the queue the object oi. For instance, η agrees with η1 • η via the queue "a"::true::3 (notation η1 • η "a"::true::3 h η ) if it agrees with (!Int.η1 ⊕ !Object.η2) • η via the queue "a"::true: indeed after branch selection (the sent value 3 is an Int) the continuation of (!Int.η1 ⊕ !Object.η2) • η is η1 • η .

The main lemma concerning the above relation says that if the type η of a channel k agrees with the type (?t1.η1 + ?t2.η2) • η of k when h maps k to the queue oi :: o, and C ≤ ti, where C is the class of oi in h, then η agrees with ηi • η when h maps k to the queue o. A session environment and a heap are well-formed if:

• the same set of channels occurs in the session environment and in the heap, • at least one between the queue of a channel and the one of its dual is empty,

• when the queue of a channel k is empty, then the queue of k relates the session type of k with the session type of k.

A standard environment, a session environment and a heap are well-formed if both the heap with the standard environment and the heap with the session environment are well-formed.

DEFINITION C.13. 1. The predicate wf(Θ; h) is defined by: wf(Θ; h) if 2. wf(Γ ; Θ; h) if wf(Γ ; h) and wf(Θ; h).

It is easy to verify that wf(Θ; h) and k ∈ dom(h) imply k ∈ dom(h).

The following key lemma states that, by reducing parallel threads in a heap which is well-formed with respect to the environments used to type the threads, we get parallel threads and heaps with the same well-formedness property. Since Γ r Θi : ei t i , by rule RECEIVEC-RT and Lemma C.6 we must have for some Θ i , η1, η2, η , t0, and y fresh in E :

• Θi = Θ i , k : (?t1.η1 + ?t2.η2) • η ,

• Γ r t0 : k.recC(x){t1 ⇒ e 1 t2 ⇒ e 2 } {k : ?t1.η1 + ?t2.η2},

• Γ , y : It is handy to take into account the order on which subexpressions of the same expression are reduced. To this aim we introduce the "follows" relation between expressions. We denote by C an arbitrary context, while E is an evaluation context. DEFINITION C. [START_REF] Dezani-Ciancaglini | A distributed object oriented language with session types[END_REF]. Let e be an expression and e1, e2 be two subexpressions of e. We say that e2 follows e1 in e if, for some arbitrary context C and evaluation context E , we have that

E [e1] = C [e2] is a subexpression of e.
It is easy to check that, if e1 and e2 are as in previous definition, then e1 needs to be reduced before e2, since e1 occurs in the hole of an evaluation context E , while e2 occurs in the hole of an arbitrary context C , and E [e1], C [e2] are two different decompositions of the same expression.

We convene that all fresh channels created reducing parallel threads take successive indexes according to the order of creation, i.e. they are named k0, k1, . . .. This means that if P, h -→ * Q, h -→ * R, h and ki is a channel created in the reduction P, h -→ * Q, h , and kj is a channel created in the reduction Q, h -→ * R, h , then i < j.

The subject of a communication expression is the channel specified in its syntax on which the communication takes place. The index of a communication expression is the index of its subject.

The following crucial lemma states that a channel and its dual cannot occur in the same thread. Moreover it states that the order on communication expression indexes agrees with the "follows" relation between expressions. PROOF.

1. Straightforward, noting that the channels k and k are introduced by the rule SESSREQ-R in two different parallel threads.

2. ∅ e : t ε implies that no channel occurs in e and so the property trivially holds. We now prove that the reduction preserves the property, namely if all the channels in the subexpressions of an expression are indexed in a not increasing order, starting from the redex to all the following expressions, in the sense of Definition C.15, then after one step of reduction we get expressions that have the same property. The proof is by case analysis on the definition of -→.

Case SESSREQ-R. We have that Let E [o.s {e : η}] be an expression in which the desired property holds. After one step of reduction, in the expression e k the new channel k is the one with the highest index and no other channel occurs in it. Moreover all communication expressions occurring in e k precede all communication expressions in E . Lastly note that by induction hypothesis the desired property holds for all communication subexpressions occurring in E .

DEFINITION 2 . 4 (

 24 Successor). Let η µ =⇒. The successor of η after µ, written η µ , is defined as: η µ = ⊕ {η | η µ =⇒ η }.

  (prefixes) π ::= u?(x : ψ) | h!e | a!(x : η) (processes) P, Q ::= 0 | π.P | P ⊕ P | P + P (public channels) a ::= x | c begin.η (private channels) h ::= x | k (channels) u ::= a | h (expressions) e ::= u | • • • (systems) S, T ::= P | S S Table

τ

  =⇒ to denoteτ -→ * (i.e., the reflexive and transitive closure of -→) and =⇒ to denote τ =⇒ -→ τ =⇒.

DEFINITION 3 . 1 (

 31 Progress Property). A system S satisfies the progress property if S τ =⇒ Σ S τ -→ implies that either S does not contain internal channels or S c(z:η)

THEOREM 3 . 2 (

 32 Subject Reduction for Processes). If Γ P : ∆ and P -→ P , then Γ P : ∆ , where ∆ ∆ . THEOREM 3.3 (Subject Reduction for Systems). If Γ S : Λ and Σ S -→ Σ S , then Γ S : Λ , where Λ Λ . The definition of together with the proofs of the above theorems are given in Appendix B.1.

LEMMA 3 . 5 .

 35 If S is initial and S τ =⇒ Σ S , and S : Λ, then Σ(k) ≤ Λ(k) for all k which occur in S .

  (class) L ::= class C C { t f; S } (session) S ::= t η s { e } (expression) e ::= x | this | o | e; e | e.f:= e | e.f | new C(e) | e.s {e : η} | e • s { k : χ} | k. sendC(e){t ⇒ e t ⇒ e} | k. recC(x){t ⇒ e t ⇒ e} (parallel threads) P ::= e | P || P Table

  During evaluation, any expression new C(o) will be replaced by a new object identifier o. The heap will then maps the object identifier o to the pair (C, f : o) of its class name C and the list of its fields with corresponding objects o; this mapping is denoted by o → (C, f : o). The form h[o → h(o)[f → o ]] denotes the update of the field f of the object o with the object o . Channel names are mapped to queues of objects: k → o. The heap produced by h[k → o] maps the channel k to the queue o. With some abuse of notation we write o :: o and o :: o to denote the queue whose first and last element is o, respectively.

B. Proofs of Section 3. 2 B. 1

 21 Proof of Subject Reduction LEMMA B.1 (Strengthening). If Γ P : (h : end • ∆), then Γ P : ∆. The core of a session stack (core(∆)) is the stack obtained by removing all ended channels. This is sound by Lemma B.1. The core of a session environment is defined similarly. DEFINITION B.2 (Core). core(∆) = ( (h : η • core(∆ )) if ∆ = (h : η • ∆ ) and η = end core(∆ ) if ∆ = (h : end • ∆ ) core(Λ) = {h : η | h : η ∈ Λ and η = end} 21 2009/1/21

  DEFINITION B.3. ∆∆ is the smallest partial order relation such that:1. core(∆ ) = (h : η • ∆ ), and core(∆) = ∆ or 2. core(∆ ) = (h : η • ∆ ), core(∆) = (h : η • ∆ ), and either η µ -→ η or η -→ η , or 3. core(∆ ) = (h : η • ∆ ), core(∆) = (h : !χ.η • (h : η • ∆ ))and η ≤ χ, or 4. core(∆ ) = (h : η • x : η ), core(∆) = (h : ?χ.η) and χ ≤ η . 5. core(∆ ) = (h : η1 • ∆ ) and core(∆) = (h : η1 + η2 • ∆ ).DEFINITION B.4. ΛΛ is the smallest partial order relation such that:1. core(Λ ) = core(Λ) ∪ {h : η}, or 2. core(Λ ) = Λ ∪{h : η }, core(Λ) = Λ ∪{h : η},and either η µ -→ η or η -→ η , or 3. core(Λ ) = Λ ∪ {h : η}, core(Λ) = Λ ∪ {h : η , h : !χ.η} and η ≤ χ, or 4. core(Λ ) = x : η ∪ {h : η}, core(Λ) = {h : ?χ.η} and χ ≤ η .

  2. If P c t ?(x:η) -→ P , then Γ P : (x : η • ∆) and t = begin.η and η η . 3. If P k!v -→ P , then Γ P : (k : η • ∆ ) and core(∆) = (k : !t.η {+ θ} • ∆ ).

  4. If Pk?(x:t) -→ P , then Γ , x : t P : (k : η • ∆ ) and core(∆) = ((k :?t.η {+ θ}) • ∆ ).

1

 1 , then Γ P : (k : η • ∆ ) and core(∆) = (k : !χ.η {+ θ} • (k : η • ∆ )) and η ≤ χ. 6. If P k?(x:χ) -→ P , then Γ P : (k : η • x : η ) and core(∆) = (k :?χ.η {+ θ}) and χ ≤ η . LEMMA B.13. Let P and Q be such that P =⇒ and Σ k : η, Q =⇒ and Σ k : θ, and η θ. Then Σ P Q τ -→. PROOF. Because of Definition B.11 and the duality between η and θ we have only to consider the following cases: 1. P k!v =⇒ and Q k?(x:t) =⇒ and v ∈ t. In this case P τ =⇒ k!(e).P , and Q τ =⇒ k?(x : η).Q {+ Q } and we conclude by the reduction rules LIFT and COMMUNI-=⇒ and Q k? z:χ =⇒ and Σ(k1) ≤ χ. In this case P τ =⇒ k! k1 .P , and Q τ =⇒ k? z : χ .Q {+ Q } and we conclude by the reduction rules LIFT and DELEGATION.

LEMMA 3 . 5

 35 If S is initial and S τ =⇒ Σ S , and S : Λ, then Σ(k) ≤ Λ(k) for all k ∈ dom(core(Λ)).

  k1) and Σ (k1) = Σ(k1). Let S T [ k 1/ z] : Λ . By Lemmas B.10 and B.9(5) and (6) we get Λ

e

  = o.η {sendC(5){e1}}; k.sendC(3){e2 k }, but e0 = o .η {o.η {sendC(5){e1}}; sendC(3){e2}} reduces to e || k.recC(x){[ o /this]e k } if recC(x){e } is the body of session η in the class of the object o.

Lemma C. 6

 6 states that the typing of E [e] can be broken down into the typing of e, and the typing of E [x]. Accordingly the environment Θ , that is used to type E [e] , can be broken down into two environments, Θ = Θ1 • Θ2, where Θ1 is used to type e, and Θ2 is used to type E [x].

LEMMA C. 9 (

 9 Term Substitution). If Γ (z : C) r e : t Θ and Γ r o : C ∅, then Γ r [ o /z]e : t Θ. The last lemma expresses a standard property about the typing of session bodies. LEMMA C.10 (Typing of Session Bodies). If stype(s, C) = η, and rtype(s, η, C) = t and sbody(s, η, C) = e, then {this : C} e : t η.

h

  (o) = (C, ) sbody(s, η , C) = e k, k ∈ h η η E [o.s {e : η}], h -→ E [e k ] || [ o /this]e k , h[k, k → ()] By AXIOM-RT, and by wf(Γ ; h) and h(o) = (C, ), we get that ∅ r o : C ∅. Since, by hypothesis Γ r E [o.s {e : η}] : t Θ, by Lemma C.6, we have that Γ r o.s {e : η} : t Θ1 and Θ = Θ1 • Θ2. From rule SESSREQ-RT we have that Θ1 = ∅, Θ2 = Θ, Γ e : t η . By Proposition C.3, Γ r e k : t {k : η }. By Lemma C.7, we have that Γ r E [e k ] : t {k : η } • Θ. Let rtype(s, η , C) = t0, then this : C e : t0 η by Lemma C.10, and this : C r e k : t0 { k : η}, by Proposition C.3. Therefore, by Lemmas C.8 and C.9, we have that Γ r [ o /this]e k : t0 { k : η}. Notice that the new heap h[k, k → ()] still agrees with Γ since the only changes are about channels.Let the last applied rule be SESSDEL-R:h(o) = (C, ) sbody(s, η, C) = e χ ≤ η E [o • s {k : χ}], h -→ E [[ o /this]e k ],h By AXIOM-RT, and by wf(Γ ; h) and h(o) = (C, ), we get that ∅ r o : C ∅. Since, by hypothesis Γ r E [o•s {k : χ}] : t Θ, by Lemma C.6, we have that Γ r o • s {k : χ} : t Θ1 and Θ = Θ1 • Θ2. From rule SESSDEL-RT we have that Θ1 = {k : η}, stype(s, C) = η and rtype(s, η, C) = t . By Lemma C.10, this : C e : t η, and this : C r e k : t {k : η}, by Proposition C.3. Therefore, by Lemmas C.8 and C.9, we have that Γ r [ o /this]e k : t {k : η}. By Lemma C.7, we have that Γ r E [[ o /this]e k ] : t Θ.Let the last applied rule be SENDCASE-R:h( k) = o h(o) = (C, ) C ≤ ti E [k.sendC(o){t1 ⇒ e1 t2 ⇒ e2}], h -→ E [ei], h[ k → o :: o]By AXIOM-RT, and by wf(Γ ; h) and h(o) = (C, ), we get that ∅ r o : C ∅. Since, by hypothesis Γ r E [k.sendC(o){t1 ⇒ e1 t2 ⇒ e2}] : t Θ, by Lemma C.6, we have that Γ r k.sendC(o){t1 ⇒ e1 t2 ⇒ e2} : t Θ1 and Θ = Θ1 • Θ2. From rule SENDC-RT we have that Θ1 = {k : !t1.η1 ⊕ !t2.η2}, Γ r ei : t {k : ηi}. By Lemma C.7, we have that Γ r E [ei] : t Θ , where Θ = {k : ηi} • Θ2. From Definition C.1, LATER-3 and LATER-4, we have that Θ Θ . Notice that the new heap h[ k → o :: o] still agrees with Γ since the only changes are about channels.Let the last applied rule be RECEIVECASE-R:h(k) = o :: o h(o) = (C, ) C ≤ ti E [k.recC(x){t1 ⇒ e1 t2 ⇒ e2}], h -→ E [[ o /x]ei], h[k → o]By AXIOM-RT, and by wf(Γ ; h) and h(o) = (C, ), we get that ∅ r o : C ∅. Applying rule SUB-RT, we get ∅ r o : Ci ∅. Since, by hypothesis Γ r E [k.recC(x){t1 ⇒ e1 t2 ⇒ e2}] : t Θ, by Lemma C.6, we have that Γ r k.recC(x){t1 ⇒ e1 t2 ⇒ e2} : t Θ1 and Θ = Θ1 • Θ2. From rule RECEIVEC-RT we have that Θ1 = {k : ?t1.η1 + ?t2.η2}, Γ , x : ti r ei : t {k : ηi}. By Lemma C.9, we have that Γ r [ o /x]ei : t {k : ηi}. By Lemma C.7, we have that Γ r E [[ o /x]ei] : t Θ , where Θ = {k : ηi} • Θ2. From Definition C.1, LATER-3 and LATER-4, we have that Θ Θ . Notice that the new heap h[k → o] still agrees with Γ since the only changes are about channels.

( ) h η if η η , 2 .

 2 ηi •η o::o i h η if (!t1.η1 ⊕ !t2.η2)•η oh η and h(oi) = (C, ) and C ≤ ti.

LEMMA C. 12 .

 12 Let η o i ::o h (?t1.η1 + ?t2.η2) • η , and h(oi) = (C, ), and C ≤ ti, then η o h ηi • η . PROOF. By induction on the length of o. The base case o = ( ) is straightforward from Definition C.11. For the induction case assume o = o :: o + : thus the hypothesis becomes η o i ::o ::o + h (?t1.η1 + ?t2.η2) • η . This relation can only have been obtained by case (2) of Definition C.11. So we have η = η + j • η * for some η + j (1 ≤ j ≤ n) and η * and h(o + ) = (C + , ) and C + ≤ t + j and (!t + η * o i ::o h (?t1.η1 + ?t2.η2) • η . By induction hypothesis we have C ≤ ti and (!t + η * o h ηi •η . Applying again Definition C.11(2) we get the result.

  ) ⇔ k∈dom(h), ∀k∈dom(Θ) : h(k) = ( ) ⇒ h( k) = ( ), ∀k∈dom(Θ) : h(k) = ( ) ⇒ Θ(k) h( k) h Θ( k).

LEMMA C. 14 .

 14 Let Γ r Θi : ei Ci, (1 ≤ i ≤ n), and assume wf(Γ ; Θ; h) where Θ = S 1≤i≤n Θi. Then if e1 || . . . || en, h -→ e 1 || . . . || e n , h there are Γ and Θ i such that Γ r Θ i : e i Ci (1 ≤ i ≤ n ), and Γ ⊆ Γ , Θ Θ and wf(Γ ; Θ ; h ), where Θ = S 1≤i≤n Θ i . PROOF. We have that, for some i (1 ≤ i ≤ n), either ei, h -→ e i || e i , h by an application of rule SESSREQ-R or ei, h -→ e i , h by the application of any one of the other reduction rules. In the former case the proof follows immediately by Theorem C.1(2) and Definition C.13. So let ei, h -→ e i , h . If this reduction has not been obtained by a communication rule the proof is trivial by Theorem C.1(1). The interesting cases are when the reduction ei, h -→ e i , h is obtained by a communication rule. RECEIVECASE-R. Assume ei = E [k.recC(x){t1 ⇒ e 1 t2 ⇒ e 2 }]. We have that E [k.recC(x){t1 ⇒ e 1 t2 ⇒ e 2 }], h -→ E [[ o /x]e j ], h , where h(k) = o :: o, and h(o) = (D, ), and h = h[k → o] and D ≤ tj.

  t0 r E [y] : ti Θ i , k : η . By the assumptions and Definitions C.13 we get that Θ( k) o::o h (?t1.η1 + ?t2.η2) • η . Then by Lemma C.12 we have that Θ( k) o h ηj • η . By rule RECEIVEC-TR we can derive Γ , x : tj r e j : t0 k : ηj. From wf(Γ ; h) and h(o) = (D, ) and D ≤ tj we get Γ r o : tj ∅ by applying AXIOM-RT and possibly SUB-RT. Then from Lemma C.9 we have that Γ r [ o /x]e j : t0 k : ηj, which implies Γ r E [[ o /x]e j ] : t i Θ i , k : ηj • η by Lemma C.7. Lastly we get Γ = Γ, and Θ i = Θ i , k : ηj • η and h (k) = o , which assure Θ Θ and wf(Γ ; Θ ; h ). SENDCR. Assume ei = E [k.sendC(o){t1 ⇒ e 1 t2 ⇒ e 2 }]. We have that E [k.sendC(o){t1 ⇒ e 1 t2 ⇒ e 2 }], h -→ E [e j ], h where h( k) = o, and h(o) = (D, ), and h = h[ k → o :: o], and D ≤ tj.Since Γ r Θi : ei t i , by rule SENDC-RT (observing that an object is typed with the empty session environment) and Lemma C.6 we must have for some Θ i , η1, η2, η , t0, and y fresh in E :• Θi = Θ i , k : (!t1.η1 ⊕ !t2.η2) • η , • Γ r k.sendC(o){t1 ⇒ e 1 t2 ⇒ e 2 } : C0 {k : !t1.η1 ⊕ !t2.η2}, • Γ , y :0 r t i : E [y] Θ i , k : η .By the assumptions and Definition C.13 we have that (!t1.η1 ⊕ !t2.η2)• η o h Θ( k), which implies ηj •η o::o h Θ( k) by Definition C.11. By rule SENDC-RT we can derive Γ r e j : t0 k : ηj, which implies Γ r E [e j ] : t i Θ i , k : ηj • η by Lemma C.7. Lastly we get Γ = Γ, and Θ i = Θ i , k : ηj • η and h ( k) = o :: o, which assure Θ Θ and wf(Γ ; Θ ; h ).

LEMMA C. 16 .

 16 Let ∅ e : t ε and e, [ ] -→ * e1 || . . . || en, h. Then:1. no expression ei can contain occurrences of both k and k for some channel k, 2. if e , e are communication subexpressions of ei and e follows e , then the index of e is greater than or equal to the index of e .

h

  (o) = (C, ) sbody(s, η , C) = e k, k ∈ h η η E [o.s {e : η}], h -→ E [e k ] || [ o /this]e k , h[k, k → ()]

  a union of sets is empty if and only if every set in the union is empty, by applying the usual De Morgan laws we can reduce this problem to deciding the inclusion V

i∈I begin.ηi <: W j∈J begin.ηj. As regards session channels, we notice that a value has type (begin.η)∧(begin.η ) if and only if it has type begin.(η⊕η ). Also note that begin.η <: begin.η1 ∨ begin.η2 if and only if begin.η <: begin.η1 or begin.η <: begin.η2 (Proposition 2.8). Therefore the semantic subtyping relation for the types of Section 2.1 is completely defined by (the semantic subtyping framework of [17] and) the following equation î∈I begin.ηi <: _ j∈J begin.ηj ⇐⇒ ∃j∈J :

  Such interferences are not avoided even when we operate with = (as opposed to ≤).

	For instance, according to rule (I6) we 2).end ⊕ ?Int.!3.end = ?Int.(end ⊕ !3.end), but √ 2).end ⊕ ?Int.!3.end) + ? have ?(Int ∨ (?(Int ∨ √ √ 2.!4.end = ?Int.(end ⊕ !3.end) + ? √ 2.!4.end. Here the action ? √ 2 is not guaranteed by ?(Int ∨ √ 2).end⊕?Int.!3.end and (I6) tells us whose consequence is that in practice the capability of ?(Int ∨ √ 2).end of receiving √

. For example, by rule (S1) we have ?Int.end ≤ ?Real.end however ?Int.end + ? √ 2.!3.end ≤ ?Real.end + ? √ 2.!3.end. The reason is that in widening ?Int.end to ?Real.end we create an interference with the term ? √ 2.!3.end because of the guaranteed action ? √ 2.

  [START_REF] Dezani-Ciancaglini | Bounded session types for object-oriented languages[END_REF] (Disjunctive normal form). A sieve is in disjunctive normal form if it is of the form W

	Next, we can check emptiness of each element of the union sep-
	arately, reducing the problem to checking the following relation:
	V i∈I ηi ≤	W j∈J ηj. Since this is equivalent to	L	i∈I ηi ≤
	W j∈J ηj, we can apply the strong disjunction property (Propo-
	sition 2.7) we stated for descriptors and obtain
		î∈I	ηi ≤	_
	Subsessioning. To decide whether two descriptors are in subses-
	sioning relation we define a normal form for descriptors and, more
	generally, sieves (the latter occurring in the prefixes of the former).
	DEFINITION 2.14 (Strong normal form). A sieve χ in disjunctive
	normal form is in strong normal form if
	1. if χ ≡	W i∈I	V	j∈J λij, then for i ∈ I, j ∈ J, λij is in strong
	normal form and	V j∈J λij = ⊥ for all i ∈ I;
	2. if χ ≡ ¬η, then η is in strong normal form;
	3. otherwise χ is either of the form	L

i∈I

V

j∈J λij, where λij denote descriptor literals, that is either η or ¬η.

j∈J ηj ⇐⇒ ∃j∈J : M i∈I ηi ≤ ηj

which is precisely the same problem that has to be solved in order to decide the subtyping relation (cf. equation (

11

)). In conclusion, in order to decide both subsieving and subtyping it suffices to decide subsessioning. i∈I !ψi.ηi{ ⊕ end} or P i∈I ?ψi.ηi{ + end}

Table 9 .

 9 OO: Channel Addition

	SESS-WF	CLASS-WF
		D ok	S ok in C
		class C D { t f; S } ok

{this : C} e : t η t η s { e } ok in C

Table 12 .

 12 OO: Well-formed Class Tables. equivalence rules asserting that parallel composition is associative and commutative: P || P1 ≡ P1 || P P || (P1 || P2) ≡ (P || P1) || P2 P ≡ P ⇒ P || P1 ≡ P || P1

  By Theorem 2.15 we may assume that η is in strong normal form. We define a function • such that η η. Regularity of η is a direct consequence of the regularity of η.

	but not of	P	By definition θ is dual of j∈J ηj, contradiction.	P i∈I ηi
	Case [INT-CHOICE]. Similar to the previous case.
	Case [*-SPLIT]. These rules never fail since they can always be
	applied.
	A.2 Proof of Proposition 2.10
	(⇒)

  duality relation, since (η, η2) ∈ C by definition of C . Let (η , η 2 ) ∈ C . Then there exists η 1 such that η η 1 and η 1 η 2 . We reason by cases on the justification of η η 1 for showing that η and η 2 satisfy at least one of the conditions of Definition 2.5. Assume that η η 1 is justified by condition (1) of Definition 2.5. Then η ⇓ and η 1 ⇓ . From η 1 η 2 we derive η 2 ⇓ hence we conclude by condition (1) of Definition 2.5. Assume that η η 1 is justified by condition (2) of Definition 2.5. Then η ↓ and η ↓ µ implies η 1 ⇓ µ and η µ η 1 µ . From η 1 η 2 we derive η 2 ⇓ µ and η 1 µ η 2 µ hence (η µ , η 2 µ ) ∈ C by definition of C and we conclude by condition (2) of Definition 2.5. (⇐) It is sufficient to show that the relation R = {(η, η ) | ∀θ : θ η ⇒ θ η } is a coinductive subsession. Let (η, η ) ∈ R and assume η for otherwise there is nothing to prove. By Theorem 2.15 we may assume that both η and η are in strong normal form. By Proposition 2.10 there exists θ such that θ η. By definition of R we deduce that θ η , hence η again by Proposition 2.10. We reason by cases on the structure of η and η . Condition (1) of Definition 2.11 is trivially satisfied since η ⇓. As regards condition (2) of Definition 2.11, assume η ⇓ µ and η µ . If µ = , then η ⇓

	Assume η ≡	P	i∈I ?ψi.ηi{ + end} and η ≡	P j∈J ?ψj.ηj{ +
	end}.

  of Definition 2.11 is trivially satisfied since η ⇓. Condition (1) and (2) of Definition 2.11 are trivially satisfied since η ⇓ and η ⇓. As regards condition (3) of Definition 2.11, for every i ∈ I let θi be an arbitrary session descriptor such that θi ηi (these descriptors exist because η ). Let θ ≡ P i∈I ?ψi.θi{ + end} where the end subterm is present only if it is present also in η. Assume by contradiction η ↓ or η ⇓ .

	Assume η ≡	L	i∈I !ψi.ηi{ ⊕ end} and η ≡	P	j∈J ?ψj.ηj{ +
	end} and η ⇓. Then θ η but θ	η , which is absurd. We conclude η ↓ and
	η ⇓ .

  ). A session environment is coherent if whenever it contains k : η it contains also k : η ∈ Λ with η η . LEMMA B.15. If S is initial and S

τ =⇒ Σ P1 . . . Pn, then Pi : ∆i for 1 ≤ i ≤ n imply:

  In the last case the coherence of Λ (assured by Lemma B.15(3)) implies the duality between ∆ l (kj) and ∆ l ( kj).The second definition gives standard conditions on well-formation of heaps and agreement between heaps and term environments.DEFINITION C.2 (Well-Formed Heap and Agreement).A term environment Γ and a heap h agree, written wf(Γ ; h), if h is wellformed and the classes of objects in h are the classes associated to them by Γ . Thus wf(Γ

	1. P l	γ =⇒ and	P l	γ =⇒;
	2. P l
					Therefore Σ
	P l P l	τ -→ by Lemma B.13.
	C. Proofs of Section 3.3
	C.1 Proof of Subject Reduction
	In order to state and prove the Subject Reduction Theorem we have
	first to introduce some definitions and propositions.
	The first definition formalises the evolution of session types and
	session environments.
	DEFINITION C.1. 1. A session type η is at a later stage than
	another session type η, η	η , if that is deducible from the
	following rules.
		LATER-0	LATER-1	LATER-2
					η η	η	η
		η ε		η η	η η
	LATER-3			LATER-4
		η η
	η.η	η .η

γ

=⇒ and P l =⇒ and Σ kj : ∆ l ( kj); 3. P l =⇒ and Σ kj : ∆ l (kj) and P l γ =⇒; 4. P l =⇒ and Σ kj : ∆ l (kj) and P l =⇒ and Σ kj : ∆ l ( kj). !t.η ⊕ !t.η ηi LATER-5 ?t.η + ?t.η ηi 2. A session environment Θ is at a later stage than another session environment Θ, Θ Θ , if (a) dom(Θ) ⊆ dom(Θ ), and (b) ∀k ∈ dom(Θ) : Θ(k) Θ (k).

2009/1/21

This shows that our duality is semantically defined: ?(Bool ∧ Int).end is not dual of !(Bool ∧ Int).end as a syntactic approach would suggest; both descriptors have no dual.3

2009/1/21

Rules (TR7-TR10) hide a circularity since both values and duals are defined in terms of the duality relation we are defining. Theorem 2.6 in Section 2.2.3 shows that this circularity is only apparent. 4 2009/1/21

2009/1/21

2009/1/21

2009/1/21

2009/1/21

2009/1/21

A special case is when the filter is precisely end: in that case the process can delegate any non active channel. 11 2009/1/21 T-AX Γ , x : t x : t T-VAL v ∈ t Γ v : t T-SUB Γ e : t t <: t Γ e : t T-SYS Γ P : ∆ ΓP : set(∆) T-PAR Γ S : Λ1 Γ T : Λ2 Γ S T : Λ1 ∪ Λ2 T-ZERO Γ 0 : -T-WEAK Γ P : ∆ h ∈ dom(∆ ∪ Γ ) Γ P : (h : end • ∆) T-INT Γ P : ∆ Γ Q : ∆ Γ P ⊕ Q : ∆ T-CONNECT-REQUEST Γ P : (x : η • ∆) Γ a : begin.η Γ a!(x : η).P : ∆ T-CONNECT-ACCEPT Γ P : (x : η • ∆) η η Γ c begin.η ?(x : η).P : ∆ T-COMM Γ * P : ∆ Γ P : ∆ T-RECEIVE Γ , x : t P : (h : η • ∆) Γ * h?(x : t).P : (h : ?t.η • ∆) T-SEND Γ e : t Γ P : (h : η • ∆) Γ * h!e.P : (h : !t.η • ∆) T-RECEIVES Γ P : (h : η • x : η ) χ ≤ η Γ * h?(x : χ).P : (h : ?χ.η) T-SENDS Γ P : (h : η • ∆) η ≤ χ Γ * h!h .P : (h : !χ.η • (h : η • ∆)) T-INTCH Γ * P : (h : η1 • ∆) Γ * Q : (h : η2 • ∆) Γ * P ⊕ Q : (h : η1 ⊕ η2 • ∆)

2009/1/21

2009/1/21 AXIOM-T Γ z : Γ (z) ε SUB-T Γ e : t η t ≤ t Γ e : t η NEWC-T fields(C) = t f Γ ei : ti ε Γ new C(e) : C ε FLD-T Γ e : t η Γ e.f : ftype r (f, t) η SEQ-T Γ e : t η Γ e : t η Γ e;e : t η • η FLDASS-T Γ e : t η Γ e : ftype w (f, t) η Γ e.f := e : ftype w (f, t) η • η SESSREQ-T Γ e : t η Γ e : t η ∀{η} ∈ stype(s, t)∃η ∈ η.η η Γ e.s {e : η} : t η SESSDEL-T Γ e : t η η ≤ χ ∀{η} ∈ stype(s, t)∃η ∈ η.χ ≤ η {η} ∈ stype(s, t) & η ∈ η & χ ≤ η =⇒ rtype(s, η , t) = t Γ e • s {χ} : t η • η SENDC-T Γ e : t1 ∨ t2 η Γ ei : t ηi Γ sendC(e){t1 ⇒ e1 t2 ⇒ e2} : t η • (!t1.η1 ⊕ !t2.η2) RECEIVEC-T Γ , x : ti ei : t ηi Γ recC(x){t1 ⇒ e1 t2 ⇒ e2} : t ?t1.η1 + ?t2.η2Table 11. OO: Typing Rules for Channel Free Expressions. AXIOM-RTΓ r z : Γ (z) ∅ SUB-RT Γ r e : t Θ t ≤ t Γ r e : t Θ NEWC-RT fields(C) = t f Γ r ei : ti ∅ Γ r new C(e) : C ∅ FLD-RT Γ r e : t Θ Γ r e.f : ftype r (f, t) Θ SEQ-RT Γ r e : t Θ Γ r e : t Θ Γ r e;e : t Θ • Θ FLDASS-RT Γ r e : t Θ Γ r e : ftype w (f, t) Θ Γ r e.f := e : ftype w (f, t) Θ • Θ SESSREQ-RT Γr e : t Θ Γ e : t η ∀{η} ∈ stype(s, t)∃η ∈ η.η η Γ r e.s {e : η} : t Θ SESSDEL-RT Γ r e : t Θ η ≤ χ ∀{η} ∈ stype(s, t)∃η ∈ η.χ ≤ η {η} ∈ stype(s, t) & η ∈ η & χ ≤ η =⇒ rtype(s, η , t) = t Γ r e • s {k : χ} : t Θ • {k : η} SENDC-RT Γ r e : t1 ∨ t2 Θ Γ r ei : t {k : ηi} Γ r k.sendC(e){t1 ⇒ e1 t2 ⇒ e2} : t Θ • {k : !t1.η1 ⊕ !t2.η2}

2009/1/21

2009/1/21

2009/1/21

2009/1/21

2009/1/21

2009/1/21

2009/1/21

2009/1/21

2009/1/21

PROOF. By cases on -→ using Lemma B.6. THEOREM 3.2 (Subject Reduction for Processes) If Γ P : ∆ and P -→ P , then Γ P : ∆ , where ∆ ∆ .

PROOF. The proof is by induction and by cases on -→. For external and internal choices we only consider the first cases of Lemma B.6( 8) and ( 9), since for the second cases the proof is similar and simpler.

Case R-CONNECT. Easy from Lemma B.9(case 1) and Definition B.3(case 1).

Case R-SEND. Easy from Lemma B.9(cases 3 and 5), and Definition B.3(cases 1 and 2).

Case R-RECEIVE. Easy from Lemma B.9(cases 2, 4 and 6) and Definition B.3(cases 1 and 2).

Case R-EXTCH. We have that Case R-EXTSEND. We have that

and Γ P + Q : ∆. We can lift the relations between reductions of processes and changes of session stacks shown in Lemma B.9 to relations between reductions of systems and changes of session environments. More precisely we can easily prove the following lemma:

S , then there are T, T and P such that S = T P T and S = T P T and P -→ P , where one or both T, T can be missing.

PROOF. The proof is by induction and by cases on -→.

Case LIFT. The result follows from Theorem 3.2, Lemma B.7 [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF] and Proposition B.5 [START_REF] Acciai | A type system for client progress in a service-oriented calculus[END_REF].

Case CONNECTION. We have that Γ S T : Λ and Case COMMUNICATION. We have that Γ S T : Λ and

Case DELEGATION. We have that Γ S T : Λ and

where

B.2 Proof of Progress

The key of our progress proof is the natural correspondence between labels of the LTS for processes and typing assumptions on internal channels in a fixed session environment.

DEFINITION B.11 (Agreement).

The agreement between the label and the assumption k : η via the session environment Σ (notation Σ k : η) is the smallest relation such that Σ(k) ≤ η and:

We use γ to range over finite sequences of labels of the shape c t ?(x : η) and c t !(x : η). LEMMA B.12. 1. If Γ * P : ∆ and core(∆) = (k : η • ∆), then P =⇒ and

PROOF. (1) The last applied rule in a derivation for P can only be one of the rules T-SEND, T-RECEIVE, T-SENDS, T-RECEIVES, T-EXTCH, T-INTCH.

In the first four cases P must be a communication process on channel k. In the last two cases the result follows by induction.

(2) From ( 1), taking into account that the last applied rule can also

be T-CONNECT-REQUEST, T-CONNECT-ACCEPT, T-EXT, T-INT. T-CONNECT,

The agreement between labels and typing assumptions is exploited in the following lemma: it assure that the parallel of processes offering labels which agree with dual assumptions always reduce in the current session environment.

In parallel we have the expression [ o /this]e k , where e is a session body, so the only channel in this expression is k. Then this reduction rule preserves the property.

Case SESSDEL-R. We have that

Let E [o • s {k : χ}] be an expression in which the desired property holds. Since o • s {k : χ} is the redex, then k is the channel with the highest index. After one step of reduction, [ o /this]e k is the first expression to be reduced next, and k is still the only channel which occurs in it.

Case SENDCASE-R. We have that

is an expression in which the desired property holds, then k is the channel with the highest index. The channel k is the only channel which occurs in the expressions e1, e2. Then, after one step of reduction the expression ei can contain only the channel k, that is the one with the highest index, or it can contain no channel, but the context is unchanged, then the property still holds.

Case RECEIVECASE-R. The proof is similar to the previous one.

In all the remaining case no channel is introduced or modified, then the property is trivially preserved.

THEOREM (Progress). If ∅ e0 : t0 ε and e0, [ ] -→ * e1 || . . . || en, h, then for each ei (1 ≤ i ≤ n) one of the following conditions holds:

• ei, h -→ P, h for some P, h ,

• ei = o for some o.

PROOF. Toward a contradiction we assume that e -→ * e1 |...| en, h which is irreducible and is not a parallel composition of objects. By Lemma C.14 we have that there are Γ , Θ1, ..., Θn and t1, ..., tn such that wf(Γ; Θ; h), where Θ = S 1≤i≤n Θi and Γ r Θi : ei ti for all 1 ≤ i ≤ n. We can assume without loss of generality that, for 1 ≤ m ≤ n, the expressions e1, ..., em are not objects. By Lemma C.14 we get wf(Θ; h). Then the evaluation of the expressions e1, ..., em can only be stopped by a receiving expression waiting for data in the associated channel. So for all 1 ≤ l ≤ m we must have e l = E[e l ], where e l is a case receiving communication expression. Let j be the highest among the indexes of the channels occurring in e1 |...| en. If both kj and kj occur in e1 |...| en, then by Lemma C.16(1) they occur in two different expressions, let them be ep and eq with 1 ≤ p = q ≤ m. By Lemma C. [START_REF] Frisch | Regular tree language recognition with static information[END_REF](2) the subjects of the two expressions e p and e q are the channels kj and kj . Moreover we must have that Θp(kj ), Θq ( kj ) are of the forms (?t 1.η1 + ?t 2.η2) • η, (?t 1.η 1 + ?t 2.η 2 ) • η , since e p and e q are case receiving expressions. If h(kj ) is not empty, then let h(kj ) = o :: o , and by Lemma C.12 h(o) = (C, -) and C ≤ t i is defined, so e p can perform a RECEIVECASE-R step against the hypothesis. Similarly if h( kj ) is not empty. Otherwise, if both h(kj ) and h( kj ) are empty, then by Lemma C.14 we get wf(Θ; h), which implies Θq ( kj ) Θp(kj ). But this is impossible since Θp(kj ) and Θq ( kj ) are of the forms (?t 1.η1 + ?t 2.η2) • η, (?t 1.η 1 + ?t 2.η 2 ) • η . If only kj occurs in e1 |...| en, then we must have Θ( kj ) = and from wf(Θ; h) get that h(kj ) is not empty, and so we can argue as before.