Comparing Deadlock-Free Session Typed Processes
Ornela Dardha

Jorge A. Pérez

University of Glasgow, United Kingdom

University of Groningen, The Netherlands

Besides respecting prescribed protocols, communication-centric systems should never “get stuck”.
This requirement has been expressed by liveness properties such as progress or (dead)lock freedom.
Several typing disciplines that ensure these properties for mobile processes have been proposed.
Unfortunately, very little is known about the precise relationship between these disciplines–and the
classes of typed processes they induce.
In this paper, we compare L and K , two classes of deadlock-free, session typed concurrent
processes. The class L stands out for its canonicity: it results naturally from interpretations of
linear logic propositions as session types. The class K , obtained by encoding session types into
Kobayashi’s usage types, includes processes not typable in other type systems.
We show that L is strictly included in K . We also identify the precise condition under which
L and K coincide. One key observation is that the degree of sharing between parallel processes
determines a new expressiveness hierarchy for typed processes. We also provide a type-preserving
rewriting procedure of processes in K into processes in L . This procedure suggests that, while
effective, the degree of sharing is a rather subtle criteria for distinguishing typed processes.

1

Introduction

The goal of this work is to formally relate different type systems for the π -calculus. Our interest
is in session-based concurrency, a type-based approach to communication correctness: dialogues between participants are structured into sessions, basic communication units; descriptions of interaction
sequences are then abstracted as session types [12] which are checked against process specifications.
We offer the first formal comparison between different type systems that enforce (dead)lock freedom,
the liveness property that ensures session communications never “get stuck”. Our approach relates the
classes of typed processes that such systems induce. To this end, we identify a property on the structure
of typed parallel processes, the degree of sharing, which is key in distinguishing two salient classes of
deadlock-free session processes, and in shedding light on their formal underpinnings.
In session-based concurrency, types enforce correct communications through different safety and
liveness properties. Basic correctness properties are communication safety and session fidelity: while the
former ensures absence of errors (e.g., communication mismatches), the latter ensures that well-typed
processes respect the protocols prescribed by session types. Moreover, a central (liveness) property for
safe processes is that they should never “get stuck”. This is the well-known progress property, which
asserts that a well-typed term either is a final value or can further reduce [17]. In calculi for concurrency,
this property has been formalized as deadlock freedom (“a process is deadlock-free if it can always reduce
until it eventually terminates, unless the whole process diverges” [15]) or as lock freedom (“a process is
lock free if it can always reduce until it eventually terminates, even if the whole process diverges” [13]).
Notice that in the absence of divergent behaviors, deadlock and lock freedom coincide.
(Dead)lock freedom guarantees that all communications will eventually succeed, an appealing requirement for communicating processes. Several advanced type disciplines that ensure deadlock-free
processes have been proposed (see, e.g., [2, 3, 5, 10, 13, 15, 16, 20]). Unfortunately, these disciplines consider different process languages and/or are based on rather different principles. As a result, very little
S. Crafa and D. Gebler (Eds.): Combined Workshop on Expressiveness in
Concurrency and Structural Operational Semantics (EXPRESS/SOS 2015)
EPTCS 190, 2015, pp. 1–15, doi:10.4204/EPTCS.190.1

© O. Dardha & J.A. Pérez
This work is licensed under the
Creative Commons Attribution License.

2

Comparing Deadlock-Free Session Typed Processes

is known about how they relate to each other. This begs several research questions: What is the formal
relationship between these type disciplines? What classes of deadlock-free processes do they induce?
In this paper, we tackle these open questions by comparing L and K , two salient classes of
deadlock-free, session typed processes (Definition 4.2):
• L contains all session processes that are well-typed according to the Curry-Howard correspondence
of linear logic propositions as session types [2, 3, 21]. This suffices, because the type system derived
from such a correspondence ensures communication safety, session fidelity, and deadlock freedom.
• K contains all session processes that enjoy communication safety and session fidelity (as ensured by
the type system of Vasconcelos [19]) and are (dead)lock-free by combining Kobayashi’s type system
based on usages [13, 15] with Dardha et al.’s encodability result [8].
There are good reasons for considering L and K . On the one hand, due to its deep logical foundations,
L appears to us as the canonic class of deadlock-free session processes, upon which all other classes
should be compared. Indeed, this class arguably offers the most principled yardstick for comparisons. On
the other hand, K integrates session type checking with the sophisticated usage discipline developed by
Kobayashi for π -calculus processes. This indirect approach to deadlock freedom (first suggested in [14],
later developed in [4, 7, 8]) is fairly general, as it may capture sessions with subtyping, polymorphism,
and higher-order communication. Also, as informally shown in [4], K strictly includes classes of typed
processes induced by other type systems for deadlock freedom in sessions [5, 10, 16].
One key observation in our development is that K corresponds to a family of classes of deadlock-free
processes, denoted K0 , K1 , · · · , Kn , which is defined by the degree of sharing between their parallel
components. Intuitively, K0 is the subclass of K with independent parallel composition: for all
processes P | Q ∈ K0 , subprocesses P and Q do not share any sessions. Then, K1 is the subclass of
K which contains K0 but admits also processes with parallel components that share at most one session.
Then, Kn contains deadlock-free session processes whose parallel components share at most n sessions.
Contributions. In this paper, we present three main contributions:
1. We show that the inclusion between the constituent classes of K is strict (Theorem 4.4). We have:
K0 ⊂ K1 ⊂ K2 ⊂ · · · ⊂ Kn ⊂ Kn+1

(1)

Although not extremely surprising, the significance of this result lies in the fact that it talks about
concurrency (via the degree of sharing) but implicitly also about the potential sequentiality of parallel
processes. As such, processes in Kk are necessarily “more parallel” than those in Kk+1 . Interestingly,
the degree of sharing in K0 , . . . , Kn can be defined in a very simple way, via a natural condition in the
rule for parallel composition in Kobayashi’s type system for deadlock freedom.
2. We show that L and K1 coincide (Theorem 4.6). That is, there are deadlock-free session processes
that cannot be typed by systems derived from the Curry-Howard interpretation of session types [2, 3,
21], but that can be admitted by the (indirect) approach of [8]. This result is significant: it establishes
the precise status of systems based on [3,21] with respect to previous (non Curry-Howard) disciplines.
Indeed, it formally confirms that linear logic interpretations of session types naturally induce the most
basic form of concurrent cooperation (sharing of exactly one session), embodied as the principle of
“composition plus hiding”, a distinguishing feature of such interpretations.
3. We define a rewriting procedure of processes in K into L (Defintion 5.7). Intuitively, due to our
previous observation and characterization of the degree of sharing in session typed processes, it is

O. Dardha & J.A. Pérez

3

quite natural to convert a process in K into another, more parallel process in L . In essence, the procedure replaces sequential prefixes with representative parallel components. The rewriting procedure
satisfies type-preservation, and enjoys the compositionality and operational correspondence criteria
as stated in [11] (cf. Theorems 5.8 and 5.10). These properties not only witness the significance of the
rewriting procedure; they also confirm that the degree of sharing is a rather subtle criteria for formally
distinguishing deadlock-free, session typed processes.
To the best of our knowledge, these contributions define the first formal comparison between fundamentally distinct type systems for deadlock freedom in session communications. Previous comparisons, such
as the ones in [4] and [3, §6], are informal: they are based on representative “corner cases”, i.e., examples
of deadlock-free session processes typable in one system but not in some other.
The paper is structured as follows. § 2 summarizes the session π -calculus and associated type system
of [19]. In § 3 we present the two typed approaches to deadlock freedom for sessions. § 4 defines the
classes L and K , formalizes the hierarchy (1), and shows that L and K1 coincide. In § 5 we give the
rewriting procedure of Kn into L and establish its properties. § 6 collects some concluding remarks.
Due to space restrictions, details of proofs are omitted; they can be found online [9].

2

Session π -calculus

Following Vasconcelos [19], we introduce the session π -calculus and its associated type system which
ensures communication safety and session fidelity. The syntax is given in Figure 1 (upper part). Let P, Q
range over processes x, y over channels and v over values; for simplicity, the set of values coincides with
that of channels. In examples, we often use n to denote a terminated channel that cannot be further used.
Process xhvi.P denotes the output of v along x, with continuation P. Dually, process x(y).P denotes
an input along x with continuation P, with y denoting a placeholder. Process x ⊳ l j .P uses x to select l j
from a labelled choice process, being x ⊲ {li : Pi }i∈I , so as to trigger Pj ; labels indexed by the finite set I
are pairwise distinct. We also have the inactive process (denoted 0), the parallel composition of P and Q
(denoted P | Q), and the (double) restriction operator, noted (ν xy)P: the intention is that x and y denote
dual session endpoints in P. We omit 0 whenever possible and write, e.g., xhni instead of xhni.0. Notions
of bound/free variables in processes are standard; we write fn(P) to denote the set of free names of P.
Also, we write P[v/z] to denote the (capture-avoiding) substitution of free occurrences of z in P with v.
The operational semantics is given in terms of a reduction relation, noted P → Q, and defined by the
rules in Figure 1 (lower part). It relies on a standard notion of structural congruence, noted ≡ (see [19]).
We write →∗ to denote the reflexive, transitive closure of →. Observe that interaction involves prefixes with different channels (endpoints), and always occurs in the context of an outermost (double)
restriction. Key rules are (R-C OM) and (R-C ASE), denoting the interaction of output/input prefixes and
selection/branching constructs, respectively. Rules (R-PAR), (R-R ES), and (R-S TR) are standard.
The syntax of session types, ranged over T, S, . . ., is given by the following grammar.
T, S ::= end

|

?T.S

|

!T.S

|

&{li : Si }i∈I

|

⊕ {li : Si }i∈I

Above, end is the type of an endpoint with a terminated protocol. The type ?T.S is assigned to an
endpoint that first receives a value of type T and then continues according to the protocol described
by S. Dually, type !T.S is assigned to an endpoint that first outputs a value of type T and then continues
according to the protocol described by S. Type ⊕{li : Si }i∈I , an internal choice, generalizes output
types; type &{li : Si }i∈I , an external choice, generalizes input types. Notice that session types describe
sequences of structured behaviors; they do not admit parallel composition operators.

Comparing Deadlock-Free Session Typed Processes

4

P, Q ::= xhvi.P
x(y).P
x ⊳ l j .P
x ⊲ {li : Pi }i∈I
v ::= x

(output)
(input)
(selection)
(branching)
(channel)

0
(inaction)
P|Q
(composition)
(ν xy)P (session restriction)

(R-C OM) (ν xy)(xhvi.P | y(z).Q) → (ν xy)(P | Q[v/z])

(R-PAR)

(R-C ASE) (ν xy)(x ⊳ l j .P | y ⊲ {li : Pi }i∈I ) → (ν xy)(P | Pj ) j ∈ I
(R-S TR) P ≡ P′ , P → Q, Q′ ≡ Q =⇒ P′ → Q′

(R-R ES) P → Q =⇒ (ν xy)P → (ν xy)Q

P → Q =⇒ P | R → Q | R

Figure 1: Session π -calculus: syntax and semantics.
( T-PAR )
( T-N IL )

x : end ⊢ST 0

( T-R ES )

Γ1 ⊢ST P

Γ2 ⊢ST Q

Γ, x : T, y : T ⊢ST P

Γ, x : S, y : T ⊢ST P

Γ ⊢ST (ν xy)P

Γ, x : ?T.S ⊢ST x(y).P

Γ1 ◦ Γ2 ⊢ST P | Q

( T-S EL )

( T-B RCH )

( T-O UT )

Γ, x : Si ⊢ST Pi

Γ, x : S ⊢ST P
Γ, x : !T.S, y : T ⊢ST xhyi.P

( T-I N )

Γ, x : S j ⊢ST P

∀i ∈ I

Γ, x : &{li : Si }i∈I ⊢ST x ⊲ {li : Pi }i∈I

∃j ∈ I

Γ, x : ⊕{li : Si }i∈I ⊢ST x ⊳ l j .P

Figure 2: Typing rules for the π -calculus with sessions.
A central notion in session-based concurrency is duality, which relates session types offering opposite
(i.e., complementary) behaviors. Duality stands at the basis of communication safety and session fidelity.
Given a session type T , its dual type T is defined as follows:
!T.S , ?T.S
⊕{li : Si }i∈I , &{li : Si }i∈I

?T.S , !T.S
&{li : Si }i∈I , ⊕{li : Si }i∈I

end , end

Typing contexts, ranged over by Γ, Γ′ , are sets of typing assignments x : T . Given a context Γ and a
process P, a session typing judgement is of the form Γ ⊢ST P. Typing rules are given in Figure 2. Rule (TN IL ) states that 0 is well-typed under a terminated channel. Rule (T-PAR) types the parallel composition of
two processes by composing their corresponding typing contexts using a splitting operator, noted ◦ [19].
Rule (T-R ES) types a restricted process by requiring that the two endpoints have dual types. Rules (TI N) and (T-O UT ) type the receiving and sending of a value over a channel x, respectively. Finally, rules
(T-B RCH) and (T-S EL) are generalizations of input and output over a labelled set of processes.
The main guarantees of the type system are communication safety and session fidelity, i.e., typed
processes respect their ascribed protocols, as represented by session types.
Theorem 2.1 (Type Preservation for Session Types). If Γ ⊢ST P and P → Q, then Γ ⊢ST Q.
The following notion of well-formed processes is key to single out meaningful typed processes.
Definition 2.2 (Well-Formedness for Sessions). A process is well-formed if for any of its structural
e
| Q) the following hold.
congruent processes of the form (ν xy)(P

• If P and Q are prefixed at the same variable, then the variable performs the same action (input or
output, branching or selection).

O. Dardha & J.A. Pérez

5

• If P is prefixed in xi and Q is prefixed in yi where xi yi ∈ xy,
e then P | Q →.

It is important to notice that well-typedness of a process does not imply the process is well-formed.
We have the following theorem:
Theorem 2.3 (Type Safety for Sessions [19]). If ⊢ST P then P is well-formed.
We present the main result of the session type system. The following theorem states that a well-typed
closed process does not reduce to an ill-formed one. It follows immediately from Theorems 2.1 and 2.3.
Theorem 2.4 ( [19]). If ⊢ST P and P →∗ Q, then Q is well-formed.
An important observation is that the session type system given above does not exclude deadlocked
processes, i.e., processes which reach a “stuck state.” This is because the interleaving of communication
prefixes in typed processes may create extra causal dependencies not described by session types. (This
intuitive definition of deadlocked processes will be made precise below.) A particularly insidious class
of deadlocks is due to cyclic interleaving of channels in processes. For example, consider a process such
as P , (ν xy)(ν wz)(xhni.whni | z(t).y(s)): it represents the implementation of two (simple) independent
sessions, which get intertwined (blocked) due to the nesting induced by input and output prefixes. We
have that n : end ⊢ST P even if P is unable to reduce. A deadlock-free variant of P would be, e.g., process
P′ , (ν xy)(ν wz)(xhni.whni | y(s).z(t)), which also is typable in ⊢ST .
We will say that a process is deadlock-free if any communication action that becomes active during
execution is eventually consumed; that is, there is a corresponding co-action that eventually becomes
available. Below we define deadlock freedom in the session π -calculus; we follow [13, 15] and consider
fair reduction sequences [6]. For simplicity, we omit the symmetric cases for input and branching.
Definition 2.5 (Deadlock Freedom for Session π -Calculus). A process P0 is deadlock-free if for any fair
reduction sequence P0 → P1 → P2 → . . ., we have that
e
| R), for i ≥ 0, implies that there exists n ≥ i such that
1. Pi ≡ (ν xy)(xhvi.Q
′
′
′ y′ )(Q | R [v/z] | R );
f
Pn ≡ (ν x y )(xhvi.Q | y(z).R1 | R2 ) and Pn+1 ≡ (ν xf
1
2

3

e
⊳ l j .Q | R), for i ≥ 0, implies that there exists n ≥ i such that
2. Pi ≡ (ν xy)(x
′
′
′ y′ )(Q | R | S).
f
Pn ≡ (ν x y )(x ⊳ l j .Q | y ⊲ {lk : Rk }k∈I∪{ j} | S) and Pn+1 ≡ (ν xf
j

Two Approaches to Deadlock Freedom

We introduce two approaches to deadlock-free, session typed processes. The first one, given in § 3.1,
comes from interpretations of linear logic propositions as session types [1–3, 21]; the second approach,
summarized in § 3.2, combines usage types for the standard π - calculus with encodings of session processes and types [8]. Based on these two approaches, in § 4 we will define the classes L and K .

3.1 Linear Logic Foundations of Session Types
The linear logic interpretation of session types was introduced by Caires and Pfenning [3], and developed
by Wadler [21] and others. Initially proposed for intutitionistic linear logic, here we consider an interpretation based on classical linear logic with mix principles, following a recent presentation by Caires [1].
The syntax and semantics of processes are as in § 2 except for the following differences. First, we
have the standard restriction construct (ν x)P, which replaces the double restriction. Second, we have a
so-called forwarding process, denoted [x ↔ y], which intuitively “fuses” names x and y. Besides these

Comparing Deadlock-Free Session Typed Processes

6

( T-1)

( T-⊥)

0 ⊢CH x:•

( T-O)

P ⊢CH ∆

( T-id)

P ⊢CH x:•, ∆

[x ↔ y] ⊢CH x:A, y:A

( T-⊗)

P ⊢CH ∆, y:A, x:B

( T-cut)

P ⊢CH ∆, y:A

x(y).P ⊢CH ∆, x:A O B

Q ⊢CH ∆′ , x:B

P ⊢CH ∆, x:A

(ν x)(P | Q) ⊢CH ∆, ∆′

x(y).(P | Q) ⊢CH ∆, ∆′ , x:A ⊗ B
( T-&)

( T-⊕)

P ⊢CH ∆, x:A j

( T-mix)

Pi ⊢CH ∆, x:Ai

j∈I

x ⊳ l j .P ⊢CH ∆, x: ⊕ {li : Ai }i∈I

Q ⊢CH ∆′ , x:A

P ⊢CH ∆

∀i ∈ I

x ⊲ {li : Pi }i∈I ⊢CH ∆, x:&{li : Ai }i∈I

Q ⊢CH ∆′

P | Q ⊢CH ∆, ∆′

Figure 3: Typing rules for the π -calculus with C-types.
differences in syntax, we have also some minor modifications in reduction rules. Differences with respect
to the language considered in § 2 are summarized in the following:
P, Q ::= (ν x)P (channel restriction)
(R-C H C OM) xhvi.P | x(z).Q → P | Q[v/z]
(R-C H C ASE) x ⊳ l j .P | x ⊲ {li : Pi }i∈I → P | Pj

|

[x ↔ y] (forwarding)
(ν x)([x ↔ y] | P) → P[y/x]
(R-C H R ES) P → Q =⇒ (ν x)P → (ν x)Q
(R-F WD)

j∈I

Observe how interaction of input/output prefixes and selection/branching is no longer covered by an
outermost restriction. As for the type system, we consider the so-called C-types which correspond to
linear logic propositions. They are given by the following grammar:
A, B ::= ⊥

|

1

|

A⊗B

|

AOB

|

⊕ {li : Ai }i∈I

|

&{li : Ai }i∈I

Intuitively, ⊥ and 1 are used to type a terminated endpoint. Type A ⊗ B is associated to an endpoint that
first outputs an object of type A and then behaves according to B. Dually, type A O B is the type of an
endpoint that first inputs an object of type A and then continues as B. The interpretation of ⊕{li : Ai }i∈I
and &{li : Ai }i∈I as select and branch behaviors follows as expected.
We define a full duality on C-types, which exactly corresponds to the negation operator of CLL (·)⊥ .
The dual of type A, denoted A, is inductively defined as follows:
1 = ⊥
A⊗B = AOB

⊥ = 1
AOB = A⊗B

⊕{li : Ai }i∈I
&{li : Ai }i∈I

= &{li : Ai }i∈I
= ⊕{li : Ai }i∈I

Recall that A⊸B , A O B. As explained in [1], considering mix principles means admitting ⊥⊸1 and
1⊸⊥, and therefore ⊥ = 1. We write • to denote either ⊥ or 1, and decree that • = •.
Typing contexts, sets of typing assignments x : A, are ranged over ∆, ∆′ , . . .. The empty context is
denoted ‘ · ’. Typing judgments are then of the form P ⊢CH ∆. Figure 3 gives the typing rules associated
to the linear logic interpretation. Salient points include the use of bound output (ν y)xhyi.P, which is
abbreviated as x(y)P. Another highlight is the “composition plus hiding” principle implemented by
rule (T-cut), which integrates parallel composition and restriction in a single rule. Indeed, there is no
dedicated rule for restriction. Also, rule (T-mix) enables the typing of independent parallel compositions,
i.e., the composition of two processes that do not share sessions.
We now collect main results for this type system; see [1, 3] for details. For any P, define live(P) if
and only if P ≡ (ν ne)(π .Q | R), where π is an input, output, selection, or branching prefix.

O. Dardha & J.A. Pérez

7

U ::= ?oκ .U (used in input)
!oκ .U (used in output)
T ::= U [Te] (channel types)

0/
(not usable)
(U1 | U2 ) (used in parallel)
hl : T ii∈I (variant type)

Figure 4: Syntax of usage types for the π -calculus.

Theorem 3.1 (Type Preservation for C-Types). If P ⊢CH ∆ and P −→ Q then Q ⊢CH ∆.
Theorem 3.2 (Progress). If P ⊢CH · and live(P) then P −→ Q, for some Q.

3.2 Deadlock Freedom by Encodability
As mentioned above, the second approach to deadlock-free session processes is indirect, in the sense that
establishing deadlock freedom for session processes appeals to usage types for the π -calculus [13,15], for
which type systems enforcing deadlock freedom are well-established. Formally, this reduction exploits
encodings of processes and types: a session process Γ ⊢ST P is encoded into a (standard) π -calculus
process JΓK f ⊢nKB JPK f . Next we introduce the syntax of standard π -calculus processes with variant
values (§ 3.2.1), the discipline of usage types (§ 3.2.2), and the encodings of session processes and types
into standard π -calculus processes and usage types, respectively (§ 3.2.3).
3.2.1

Processes

The syntax and semantics of the π - calculus with usage types build upon those in § 2. We require some
modifications. First, the encoding of terms presented in § 3.2.3, requires polyadic communication. Rather
than branching and selection constructs, the π - calculus that we consider here includes a case construct
case v of {li xi ⊲Pi }i∈I that uses variant value l j v. Moreover, we consider the standard channel restriction,
rather than double restriction. These modifications are summarized below:
P, Q ::= (ν x)P (channel restriction)
v ::= l j v
(variant value)

|

case v of {li xi ⊲ Pi }i∈I

vi.P | x(e
z).Q → P | Q[ve/ez]
(Rπ - C OM) xhe
(Rπ - R ES) P → Q =⇒ (ν x)P → (ν x)Q
(Rπ - C ASE) case l j v of {li xi ⊲ Pi }i∈I → Pj [v/xi ]

(case)

j∈I

The definition of deadlock-freedom for the π -calculus follows [13, 15]:
Definition 3.3 (Deadlock Freedom for Standard π -Calculus). A process P0 is deadlock-free under fair
scheduling, if for any fair reduction sequence P0 → P1 → P2 → · · · the following hold
1. if Pi ≡ (ν x̃)(xhe
vi.Q | R) for i ≥ 0, implies that there exists n ≥ i such that
Pn ≡ (ν x̃)(xhe
vi.Q | x(e
z).R1 | R2 ) and Pn+1 ≡ (ν x̃)(Q | R1 [ve/ez] | R2 );

z).Q | R) for i ≥ 0, implies that there exists n ≥ i such that
2. if Pi ≡ (ν x̃)(x(e
z).Q | xhe
vi.R1 | R2 ) and Pn+1 ≡ (ν x̃)(Q[ve/ez] | R1 | R2 ).
Pn ≡ (ν x̃)(x(e

3.2.2

Usage Types

The syntax of usage types is defined in Figure 4. For simplicity, we let α range over input ? or output
! actions. The usage 0/ describes a channel that cannot be used at all. We will often omit 0,
/ and so we

Comparing Deadlock-Free Session Typed Processes

8

will write U instead of U.0.
/ Usages ?oκ .U and !oκ .U describe channels that can be used once for input
and output, respectively and then used according to the continuation usage U . The obligation o and
capability κ range over the set of natural numbers. The usage U1 | U2 describes a channel that is used
according to U1 by one process and U2 by another processes in parallel.
Intuitively, obligations and capabilities describe inter-channel dependencies:
• An obligation of level n must be fulfilled by using only capabilities of level less than n. Said differently,
an action of obligation n must be prefixed by actions of capabilities less than n.
• For an action with capability of level n, there must exist a co-action with obligation of level less than
or equal to n.
Typing contexts are sets of typing assignments and are ranged over Γ, Γ′ . A typing judgement is of the
form Γ ⊢nKB P: the annotation n explicitly denotes the greatest degree of sharing admitted in parallel processes. Before commenting on the typing rules (given in Figure 5), we discuss some important auxiliary
notions, extracted from [13, 15]. First, the composition operation on types (denoted | , and used in rules
Tπ -(PAR)n and Tπ -(O UT)) is based on the composition of usages and is defined as follows:
U1 [Te] | U2 [Te] = (U1 | U2 )[Te]

hli : Ti ii∈I | hli : Ti ii∈I = hli : Ti ii∈I

The generalization of | to typing contexts, denoted (Γ1 | Γ2 )(x), is defined as expected. The unary
operation ↑ t applied to a usage U lifts its obligation level up to t; it is defined inductively as:
↑ t 0/ = 0/

max(o,t)

↑ t ακo .U = ακ

↑ t (U1 | U2 ) = (↑t U1 | ↑t U2 )

.U

The ↑ t is extends to types/typing contexts as expected. Duality on usage types simply exchanges ? and !:
0[]
/ = 0[]
/

?oκ .U [Te] = !κo .U [Te]

!κo .U [Te] = ?κo .U [Te]

Operator “ ; ” in ∆ = x : [T ]ακo ; Γ, used in rules (Tπ -I N) and (Tπ -O UT), is such that the following hold:
dom(∆) = {x} ∪ dom(Γ)

∆(x) =

(

ακo .U [Te] if Γ(x) = U [Te]
ακo [Te]
if x ∈
/ dom(Γ)

∆(y) =↑κ +1 Γ(y) if y 6= x

The final required notion is that of a reliable usage. It builds upon the following definition:
Definition 3.4. Let U be a usage. The input and output obligation levels (resp. capability levels) of U ,
written ob? (U ) and ob! (U ) (resp. cap? (U ) and cap! (U )), are defined as:
obα (ακo .U ) = o
obα (U1 | U2 ) = min(obα (U1 ), obα (U2 ))

capα (ακo .U ) = κ
capα (U1 | U2 ) = min(capα (U1 ), capα (U2 ))

The definition of reliable usages depends on a reduction relation on usages, noted U → U ′ . Intuitively,
U → U ′ means that if a channel of usage U is used for communication, then after the communication
′
occurs, the channel should be used according to usage U ′ . Thus, e.g., ?κo .U1 | ?oκ ′ .U2 reduces to U1 | U2 .
Definition 3.5 (Reliability). We write conα (U ) when obα (U ) ≤ capα (U ). We write con(U ) when
con? (U ) and con! (U ) hold. Usage U is reliable, noted rel(U ), if con(U ′ ) holds ∀U ′ such that U →∗ U ′ .

O. Dardha & J.A. Pérez

9

( Tπ -PARn )
( Tπ -N IL )

x : 0[]
/ ⊢nKB 0

Γ1 ⊢nKB P
Γ2 ⊢nKB Q
|Γ1 ∩ Γ1 | ≤ n

( Tπ -R ES )

Γ, x : U [Te] ⊢nKB P rel(U )
Γ ⊢nKB (ν x)P

Γ1 | Γ2 ⊢nKB P | Q
( Tπ -C ASE )

( Tπ -O UT )

Γ1 ⊢nKB ṽ : Te
Γ2 ⊢nKB P
x : !κ0 [Te] ; (Γ1 | Γ2 ) ⊢nKB xhṽi.P

( Tπ -LVAL )

Γ ⊢nKB v : T j

Γ

⊢nKB l j

∃j ∈ I

v : hli : Ti ii∈I

( Tπ -I N )

Γ, ye : Te ⊢nKB P
x : ?0κ [Te] ; Γ ⊢nKB x(ỹ).P

Γ1 ⊢nKB v : hli : Ti ii∈I
Γ2 , xi : Ti ⊢nKB Pi ∀i ∈ I

Γ1 , Γ2 ⊢nKB case v of {li xi ⊲ Pi }i∈I

Figure 5: Typing rules for the π -calculus with usage types with degree of sharing n.

Typing Rules. The typing rules for the standard π - calculus with usage types are given in Figure 5.
The only difference with respect to the rules in Kobayashi’s systems [13, 15] is that we annotate typing
judgements with the degree of sharing, explicitly stated in rule (Tπ -PARn )–see below. Rule (Tπ - N IL) states
that the terminated process is typed under a terminated channel. Rule (Tπ - R ES) states that process (ν x)P
is well-typed if the usage for x is reliable (cf. Definition 3.5). Rules (Tπ - I N) and (Tπ - O UT) type input and
output processes in a typing context where the “ ; ” operator is used in order to increase the obligation
level of the channels in continuation P. Rules (Tπ - LVAL) and (Tπ - C ASE) type a choice: the first types a
variant value with a variant type; the second types a case process using a variant value as its guard.
Given a degree of sharing n, rule (Tπ -PARn) states that the parallel composition of processes P and Q
(typable under contexts Γ1 and Γ2 , respectively) is well-typed under the typing context Γ1 | Γ2 only if
|Γ1 ∩ Γ2 | ≤ n. This allows to simply characterize the “concurrent cooperation” between P and Q. As a
consequence, if P ⊢nKB then P ⊢kKB , for any k ≤ n. Observe that the typing rule for parallel composition
in [13, 15] is the same as (Tπ -PARn ), except for condition |Γ1 ∩ Γ2 | ≤ n, which is not specified.
The next theorems imply that well-typed processes by the type system in Figure 5 are deadlock-free.
Theorem 3.6 (Type Preservation for Usage Types). If Γ ⊢nKB P and P → Q, then Γ′ ⊢nKB Q for some Γ′
such that Γ → Γ′ .
Theorem 3.7 (Deadlock Freedom). If 0/ ⊢nKB P and either P ≡ (ν x̃)(x(e
z).Q | R) or P ≡ (ν x̃)(xhe
vi.Q | R),
then P → Q, for some Q.
Corollary 3.8. If 0/ ⊢nKB P, then P is deadlock-free, in the sense of Definition 3.3.
Theorem 3.2 (progress for the linear logic system) and Theorem 3.7 (deadlock freedom for the standard π -calculus) have a rather similar formulation: both properties state that processes can always reduce
if they are well-typed (under the empty typing context) and have an appropriate structure (i.e., condition
live(P) in Theorem 3.2 and condition P ≡ (ν x̃)(x(e
z).Q | R) or P ≡ (ν x̃)(xhe
vi.Q | R) in Theorem 3.7).
3.2.3

Encodings of Processes and Types

Encoding of Processes. To relate classes of processes obtained by the different type systems given so
far, we rewrite a session typed or C-typed process into a usage typed process by following a continuationpassing style: this allows us to mimic the structure of a session or C-type by sending its continuation as
a payload over a channel. This idea, suggested in [14] and developed in [8], is recalled in Figure 6.

Comparing Deadlock-Free Session Typed Processes

10

Jxhvi.PK f
Jx(y).PK f
Jx ⊳ l j .PK f

, (ν c) fx hv, ci.JPK f ,{x7→c}
, fx (y, c).JPK f ,{x7→c}
, (ν c) fx hl j ci.JPK f ,{x7→c}

Jx ⊲ {li : Pi }i∈I K f
J(ν xy)PK f
JP | QK f

, fx (y). case y of {li c ⊲ JPi K f ,{x7→c} }i∈I
, (ν c)JPK f ,{x,y7→c}
, JPK f | JQK f

Figure 6: Encoding of session processes into π -calculus processes.

/
JendKsu = 0[]
J?T.SKsu =
J!T.SKsu =
J&{li : Si }i∈I Ksu =
J⊕{li : Si }i∈I Ksu =

?κo [JT Ksu , JSKsu ]
!oκ [JT Ksu , JSKsu ]
?oκ [hli : JSi Ksu ii∈I ]
!oκ [hli : JSi Ksu ii∈I ]

JendKc = •
J?T.SKc = JT Kc O JSKc
J!T.SKc = JT Kc ⊗ JSKc
J&{li : Si }i∈I Kc = &{li : JSi Kc }i∈I
J⊕{li : Si }i∈I Kc = ⊕{li : JSi Kc }i∈I

Figure 7: Encodings of session types into usage types (Left) and C-types (Right).
Encoding of Types. We formally relate session types and logic propositions to usage types by means
of the encodings given in Figure 7. The former one, denoted as denoted J·Ksu , is taken from [8].
Definition 3.9. Let Γ be a session typing context. The encoding J·K f into usage typing context and J·Kc
into C-typing context is inductively defined as follows:
J0K
/ f = J0K
/ c , 0/

JΓ, x : T K f , JΓK f , fx : JT Ksu

JΓ, x : T Kc , JΓKc, x : JT Kc

Lemma 3.10 (Duality and encoding of session types). Let T, S be finite session types.
Then: (i) T = S if and only if JT Kc = JSKc ; (ii) T = S if and only if JT Ksu = JSKsu .
On Deadlock Freedom by Encoding. The next results relate deadlock freedom, typing and encoding.
Proposition 3.11. Let P be a deadlock-free session process, then JPK f is a deadlock-free π -process.
Proof. Follows by the encoding of terms given in Figure 6, Definition 2.5 and Definition 3.3.
Next we recall an important result relating deadlock freedom and typing, by following [4].
Corollary 3.12. Let ⊢ST P be a session process. If ⊢nKB JPK f is deadlock-free then P is deadlock-free.

4

A Hierarchy of Deadlock-Free Session Typed Processes

Preliminaries. To formally define the classes L and K , we require some auxiliary definitions. The
following translation addresses minor syntactic differences between session typed processes (cf. § 2)
and the processes typable in the linear logic interpretation of session types (cf. § 3.1). Such differences
concern output actions and the restriction operator:
Definition 4.1. Let P be a session process. The translation {{·}} is defined as
{{xhyi.P}} = x(z).([z ↔ y] | {{P}})

{{(ν xy)P}} = (ν w){{P}}[w/x][w/y] w 6∈ fn(P)

and as an homomorphism for the other process constructs.

O. Dardha & J.A. Pérez

11

Let J·Kc denote the encoding of session types into linear logic propositions in Figure 7 (right). Recall
that J·K f stands for the encoding of processes and J·Ksu for the encoding of types, both defined in [8], and
given here in Figure 6 and Figure 7 (left), respectively. We may then formally define the languages under
comparison as follows:
Definition 4.2 (Typed Languages). The languages L and Kn (n ≥ 0) are defined as follows:

L =
P | ∃Γ. (Γ ⊢ST P ∧ {{P}} ⊢CH JΓKc)

Kn =
P | ∃Γ, f . (Γ ⊢ST P ∧ JΓK f ⊢nKB JPK f )

Main Results.

Our first observation is that there are processes in K2 but not in K1 :

Lemma 4.3. K1 ⊂ K2 .
Proof. K2 contains (deadlock-free) session processes not captured in K1 . A representative example is:
P2 = (ν a1 b1 )(ν a2 b2 )(a1 (x). a2 hxi | b1 hni. b2 (z))
This process is not in K1 because it involves the composition of two parallel processes which share two
sessions. As such, it is typable in ⊢nKB (with n ≥ 2) but not in ⊢1KB .
The previous result generalizes easily, so as to define a hierarchy of deadlock-free, session processes:
Theorem 4.4. For all n ≥ 1, we have that Kn ⊂ Kn+1 .
Proof. Immediate by considering one of the following processes, which generalize process P2 in
Lemma 4.3:
Pn+1 = (ν a1 b1 )(ν a2 b2 ) · · · (ν an+1 bn+1 )(a1 (x). a2 hxi. · · · . an+1 hyi | b1 hni. b2 (z). · · · bn+1 (z))
Qn+1 = (ν a1 b1 )(ν a2 b2 ) · · · (ν an+1 bn+1 )(a1 (x). a2 hxi. · · · . an+1 (y) | b1 hni. b2 (z). · · · bn+1 hni)
To distinguish Kn+1 from Kn , we consider Pn+1 if n + 1 is even and Qn+1 otherwise.
One main result of this paper is that L and K1 coincide. Before stating this result, we make the
following observations. The typing rules for processes in L do not directly allow free output. However, free output is representable (and typable) by linear logic types by means of the transformation in
Definition 4.1. Thus, considered processes are not syntactically equal. In L there is cooperating composition (enabled by rule (T-cut) in Figure 3); independent composition can only be enabled by rule (T-mix).
Arbitrary restriction is not allowed; only restriction of parallel processes.
The following property is key in our developments: it connects our encodings of (dual) session
types into usage types with reliability (Definition 3.5), a central notion to the type system for deadlock
freedom in Figure 5. Recall that, unlike usage types, there is no parallel composition operator at the level
of session types.
Proposition 4.5. Let T be a session type. Then rel(JT Ksu | JT Ksu ) holds.
Proof (Sketch). By induction on the structure of session type T and the definitions of J·Ksu and predicate
rel(·), using Lemma 3.10 (encodings of types preserve session type duality). See [9] for details.
We then have the following main result, whose proof is detailed in [9]:
Theorem 4.6. L = K1 .

Comparing Deadlock-Free Session Typed Processes

12

Therefore, we have the following corollary, which attests that the class of deadlock-free session
processes naturally induced by linear logic interpretations of session types is strictly included in the class
induced by the indirect approach of Dardha et al. [8] (cf. § 3.2).
Corollary 4.7. L ⊂ Kn , n > 1.
The fact that (deadlock-free) processes such as P2 (cf. Lemma 4.3) are not in L is informally discussed
in [3, §6]. However, [3] gives no formal comparisons with other classes of deadlock-free processes.

5

Rewriting Kn into L

The hierarchy of deadlock-free session processes established by Theorem 4.4 is subtle in the following
sense: if P ∈ Kk+1 but P 6∈ Kk (with k ≥ 1) then we know that there is a subprocess of P that needs to
be “adjusted” in order to “fit in” Kk . More precisely, we know that such a subprocess of P must become
more independent in order to be typable under the lesser degree of sharing k.
Here we propose a rewriting procedure that converts processes in Kn into processes in K1 (that
is, L , by Theorem 4.6). The rewriting procedure follows a simple idea: given a parallel process as
input, return as output a process in which one of the components is kept unchanged, but the other is
replaced by parallel representatives of the sessions implemented in it. Such parallel representatives are
formally defined as characteristic processes and catalyzers, introduced next. The rewriting procedure is
type preserving and satisfies operational correspondence (cf. Theorems 5.8 and 5.10).

5.1 Preliminaries: Characteristic Processes and Catalyzers
Before presenting our rewriting procedure, let us first introduce some preliminary results.
Definition 5.1 (Characteristic Processes of a Session Type). Let T be a session type (cf. § 2). Given a
name x, the set of characteristic processes of T , denoted {|T |}x , is inductively defined as follows:
{|end|}x
{|?T.S|}x
{|!T.S|}x
{|&{li : Si }i∈I |}x
{| ⊕ {li : Si }i∈I |}x

=
=
=
=
=


P | P ⊢CH x: •
c
x(y).P | P ⊢CH y:JT Kc , x:JSK
y ∧ Q ∈ {|S|}x
x(y).(P
|
Q)
|
P
∈
{
|T
|
}

x ⊲ {l : P } | ∀i ∈ I. Pi ∈ {|Si |}x
S  i i i∈I
x
i∈I x ⊳ li .Pi | Pi ∈ {|Si |}

Definition 5.2 (Catalyzer). Given a session typing context Γ, we define its associated catalyzer as a
process context CΓ [·], as follows:
C0/ [·] = [·]

CΓ,x:T [·] = (ν x)(CΓ [·] | P) with P ∈ {|T |}x

We record the fact that characteristic processes are well-typed in the system of § 3.1:
Lemma 5.3. Let T be a session type. For all P ∈ {|T |}x , we have: P ⊢CH x : JT Kc
We use {|T |}x ⊢CH x : JT Kc to denote the set of processes P ∈ {|T |}x such that P ⊢CH x : JT Kc .
 
Lemma 5.4 (Catalyzers Preserve Typability). Let Γ ⊢ST P and Γ′ ⊆ Γ. Then CΓ′ P ⊢CH JΓKc \ JΓ′ Kc .
 
/
Corollary 5.5. Let Γ ⊢ST P. Then CΓ P ⊢CH 0.

O. Dardha & J.A. Pérez

13

5.2 Rewriting Kn in L
We start this section with some notations. First, in order to represent pseudo-non deterministic binary
choices between two equally typed processes, we introduce the following:
Notation 5.6. Let P1 , P2 be two processes such that k 6∈ fn(P1 , P2 ). We write P1 kk P2 to stand for the
process (ν k)(k ⊳ inx.0 | k ⊲ {inl : P1 , inr : P2 }), where label inx stands for either inl or inr.
Clearly, since session execution is purely deterministic, notation P1 kk P2 denotes that either P1 or
P2 will be executed (and that the actual deterministic choice is not relevant). It is worth adding that
Caires has already developed the technical machinery required to include non deterministic behavior
into the linear logic interpretation of session types; see [1]. Casting our rewriting procedure into the
typed framework of [1], so as to consider actual non deterministic choices, is interesting future work.
We find it convenient to annotate bound names in processes with session types, and write (ν xy : T )P
and x(y : T ).P, for some session type T . When the reduction relation involves a left or right choice
in a binary labelled choice, as in reductions due to pseudo-non deterministic choices (Notation 5.6), we
sometimes annotate the reduction as →inl or →inr . We let C denote a process context, i.e., a process with
a hole. And finally, for a typing context Γ, we shall write {|Γ|} to denote the process ∏(wi :Ti )∈Γ {|Ti |}wi .
We are now ready to give the rewriting procedure from Kn to L .
Definition 5.7 (Rewriting Kn into L ). Let P ∈ Kn such that Γ ⊢ST P, for some Γ. The encoding LΓ ⊢ST PM
is a process of L inductively defined as follows:
Lx : end ⊢ST 0M , 0

LΓ ⊢ST xhvi.P′ M , x(z). [v ↔ z] | LΓ′ , x : S ⊢ST P′ M

Γ = Γ′ , x : ?T.S

LΓ ⊢ST x ⊳ l j .P′ M , x ⊳ l j .LΓ′ , x : S j ⊢ST P′ M

Γ = Γ′ , x : ⊕{li : Si }i∈I

LΓ ⊢ST x(y : T ).P′ M , x(y).LΓ′ , x : S, y : T ⊢ST P′ M

LΓ ⊢ST x ⊲ {li : Pi }i∈I M , x ⊲ {li : LΓ′ , x : Si ⊢ST Pi M}i∈I


e | Q)M , {|Γ2 |} | C e LΓ1 , xe:Se ⊢ST PM[ez/xe]
e : S)(P
LΓ ⊢ST (ν xy
e
z:S


kk {|Γ1 |} | Cez:Ve LΓ2 , ye:Ve ⊢ST QM[ez/ye]

Γ = Γ′ , x : !T.S, v : T

Γ = Γ′ , x : &{li : Si }i∈I
Γ = Γ1 ◦ Γ2 ∧ Γ1 , xe : Se ⊢ST P
Γ2 , ye : Ve ⊢ST Q ∧Vi = Si

We illustrate the procedure in [9]. Notice that the rewriting procedure given in Definition 5.7 satisfies the compositionality criteria given in [11]. In particular, it is easy to see that the rewriting of
a composition of terms is defined in terms of the rewriting of the constituent subterms. Indeed, e.g.,
LΓ1 ◦ Γ2 ⊢ST (ν xy : S)(P | Q)M depends on a context including both LΓ1 , x : S ⊢ST PM and LΓ2 , y : S ⊢ST QM.
We present two important results about our rewriting procedure. First, we show it is type preserving:
Theorem 5.8 (Rewriting is Type Preserving). Let (Γ ⊢ST P) ∈ Kn . Then, LΓ ⊢ST PM ⊢CH JΓKc.
Notice that the inverse of the previous theorem is trivial by following the definition of typed encoding.
Theorem 5.8 is meaningful, for it says that the type interface of a process (i.e., the set of sessions implemented in it) is not modified by the rewriting procedure. That is, the procedure modifies the process
structure by closely following the causality relations described by (session) types. Notice that causality
relations present in processes, but not described at the level of types, may be removed.
The rewriting procedure also satisfies an operational correspondence result. Let us write Γ ⊢ST P1 , P2
whenever both Γ ⊢ST P1 and Γ ⊢ST P2 hold. We have the following auxiliary definition:

Comparing Deadlock-Free Session Typed Processes

14

Definition 5.9. Let P, P′ be such that Γ ⊢ST P, P′ . Then, we write P + P′ if and only if P = C[Q] and
P′ = C[Q′ ], for some context C, and there is Γ′ such that Γ′ ⊢ST Q, Q′ .
Theorem 5.10 (Operational Correspondence). Let P ∈ Kn such that Γ ⊢ST P for some Γ. Then we have:
I) If P → P′ then there exist Q, Q′ s.t. (i) LΓ ⊢ST PM →inx →∗ ≡ Q; (ii) Q + Q′ ; (iii) LΓ ⊢ST P′ M →inx Q′ .
II) If LΓ ⊢ST PM →inx →∗ ≡ Q then there exists P′ s.t. P → P′ and Q + LΓ ⊢ST P′ M.

6

Concluding Remarks

We have presented a formal comparison of fundamentally distinct type systems for deadlock-free, session
typed processes. To the best of our knowledge, ours is the first work to establish precise relationships of
this kind. Indeed, prior comparisons between type systems for deadlock freedom are informal, given in
terms of representative examples typable in one type system but not in some other.
An immediate difficulty in giving a unified account of different typed frameworks for deadlock freedom is the variety of process languages, type structures, and typing rules that define each framework.
Indeed, our comparisons involve: the framework of session processes put forward by Vasconcelos [19];
the interpretation of linear logic propositions as session types by Caires [1]; the π -calculus with usage
types defined by Kobayashi in [13]. Finding some common ground for comparing these three frameworks is not trivial—several translations/transformations were required in our developments to account
for numerous syntactic differences. We made an effort to follow the exact definitions in each framework.
Overall, we believe that we managed to concentrate on essential semantic features of two salient classes
of deadlock-free session processes, noted L and K .
Our main contribution is identifying the degree of sharing as a subtle, important issue that underlies
both session typing and deadlock freedom. We propose a simple characterization of the degree of sharing: in essence, it arises via an explicit premise for the typing rule for parallel composition in the type
system in [13]. The degree of sharing is shown to effectively induce a strict hierarchy of deadlock-free
session processes in K , as resulting from the approach of [8]. We showed that the most elementary (and
non trivial) member of this hierarchy precisely corresponds to L –arguably the most canonical class of
session typed processes known to date. Furthermore, by exhibiting an intuitive rewriting procedure of
processes in K into processes in L , we demonstrated that the degree of sharing is a subtle criteria for
distinguishing deadlock-free processes. As such, even if our technical developments are technically simple, in our view they substantially clarify our understanding of type systems for liveness properties (such
as deadlock freedom) in the context of π -calculus processes.
As future work, we would like to obtain semantic characterizations of the degree of sharing, in
the form of, e.g., preorders on typed processes that distinguish when one process “is more parallel”
than another. We plan also to extend our formal relationships to cover typing disciplines with infinite
behavior. We notice that the approach of [8] extends to recursive behavior [7] and that infinite (yet non
divergent) behavior has been incorporated into logic-based session types [18]. Finally, we plan to explore
whether the rewriting procedure given in § 5 could be adapted into a deadlock resolution procedure.
Acknowledgements. We are grateful to Luı́s Caires, Simon J. Gay, and the anonymous reviewers for
their valuable comments and suggestions. This work was partially supported by the EU COST Action
IC1201 (Behavioural Types for Reliable Large-Scale Software Systems). Dardha is supported by the
UK EPSRC project EP/K034413/1 (From Data Types to Session Types: A Basis for Concurrency and
Distribution). Pérez is also affiliated to NOVA Laboratory for Computer Science and Informatics, Universidade Nova de Lisboa, Portugal.

O. Dardha & J.A. Pérez

15

References
[1] Luı́s Caires (2014): Types and Logic, Concurrency and Non-Determinism.
In Essays for the
Luca Cardelli Fest - Microsoft Research Technical Report MSR-TR-2014-104.
Available at
http://research.microsoft.com/apps/pubs/default.aspx?id=226237.
[2] Luı́s Caires & Frank Pfenning (2010): Session Types as Intuitionistic Linear Propositions. In: Proc. of
CONCUR 2010, LNCS 6269, Springer, pp. 222–236, doi:10.1007/978-3-642-15375-4 16.
[3] Luı́s Caires, Frank Pfenning & Bernardo Toninho (2014): Linear Logic Propositions as Session Types.
MSCS, doi:10.1017/S0960129514000218.
[4] Marco Carbone, Ornela Dardha & Fabrizio Montesi (2014): Progress as Compositional Lock-Freedom. In:
COORDINATION, LNCS 8459, Springer, pp. 49–64, doi:10.1007/978-3-662-43376-8 4.
[5] Marco Carbone & Søren Debois (2010): A Graphical Approach to Progress for Structured Communication
in Web Services. In: Proc. of ICE 2010, Amsterdam, The Netherlands, 10th of June 2010., EPTCS 38, pp.
13–27, doi:10.4204/EPTCS.38.4.
[6] Gerardo Costa & Colin Stirling (1987): Weak and Strong Fairness in CCS. Inf. Comput. 73(3), pp. 207–244,
doi:10.1016/0890-5401(87)90013-7.
[7] Ornela Dardha (2014): Recursive Session Types Revisited. In: Proceedings Third Workshop on Behavioural
Types, BEAT 2014, Rome, Italy, 1st September 2014., EPTCS 162, pp. 27–34, doi:10.4204/EPTCS.162.4.
[8] Ornela Dardha, Elena Giachino & Davide Sangiorgi (2012): Session types revisited. In: Proc. of PPDP’12,
ACM, pp. 139–150, doi:10.1145/2370776.2370794.
[9] Ornela Dardha & Jorge A. Pérez (2015): Full version of this paper. Technical Report. Available at
http://www.jorgeaperez.net.
[10] Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro & Nobuko Yoshida (2008): On Progress for Structured Communications. In: Trustworthy Global Computing, LNCS 4912, Springer, pp. 257–275,
doi:10.1007/978-3-540-78663-4 18.
[11] Daniele Gorla (2010): Towards a unified approach to encodability and separation results for process calculi.
Inf. Comput. 208(9), pp. 1031–1053, doi:10.1016/j.ic.2010.05.002.
[12] Kohei Honda, Vasco Thudichum Vasconcelos & Makoto Kubo (1998): Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Proc. of ESOP’98, LNCS 1381, Springer, pp.
122–138, doi:10.1007/BFb0053567.
[13] Naoki Kobayashi (2002): A Type System for Lock-Free Processes. Inf. Comput. 177(2), pp. 122–159,
doi:10.1006/inco.2002.3171.
[14] Naoki Kobayashi (2003): Type Systems for Concurrent Programs. In: Formal Methods at the Crossroads,
LNCS 2757, Springer, pp. 439–453, doi:10.1007/978-3-540-40007-3 26.
[15] Naoki Kobayashi (2006): A New Type System for Deadlock-Free Processes. In: Proc. of CONCUR 2006,
LNCS 4137, Springer, pp. 233–247, doi:10.1007/11817949 16.
[16] Luca Padovani (2013): From Lock Freedom to Progress Using Session Types. In: Proceedings of PLACES
2013, Rome, Italy, 23rd March 2013., EPTCS 137, pp. 3–19, doi:10.4204/EPTCS.137.2.
[17] Benjamin C. Pierce (2002): Types and programming languages. MIT Press, MA, USA.
[18] Bernardo Toninho, Luı́s Caires & Frank Pfenning (2014): Corecursion and Non-divergence in Session-Typed
Processes. In: Proc. of TGC 2014, LNCS 8902, Springer, pp. 159–175, doi:10.1007/978-3-662-45917-1 11.
Inf. Comput. 217, pp. 52–70,
[19] Vasco T. Vasconcelos (2012): Fundamentals of session types.
doi:10.1016/j.ic.2012.05.002.
[20] Hugo Torres Vieira & Vasco Thudichum Vasconcelos (2013): Typing Progress in Communication-Centred
Systems. In: COORDINATION, LNCS 7890, Springer, pp. 236–250, doi:10.1007/978-3-642-38493-6 17.
[21] Philip Wadler (2012):
Propositions as sessions.
doi:10.1145/2364527.2364568.

In:

Proc. of ICFP’12,

pp. 273–286,

