A New Linear Logic for Deadlock-Free Session-Typed Processes

  • Ornela Dardha
  • Simon J. Gay
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10803)


The \(\pi \)-calculus, viewed as a core concurrent programming language, has been used as the target of much research on type systems for concurrency. In this paper we propose a new type system for deadlock-free session-typed \(\pi \)-calculus processes, by integrating two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom by forbidding cyclic process connections. The second is Kobayashi’s approach in which types are annotated with priorities so that the type system can check whether or not processes contain genuine cyclic dependencies between communication operations. We combine these two techniques for the first time, and define a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities. This can be seen in three ways: (i) as a new linear logic in which cyclic structures can be derived and a \(\small \textsc {Cycle}\)-elimination theorem generalises \(\small \textsc {Cut}\)-elimination; (ii) as a logically-based session type system, which is more expressive than Caires and Pfenning’s; (iii) as a logical foundation for Kobayashi’s system, bringing it into the sphere of the propositions-as-types paradigm.

1 Introduction

The Curry-Howard correspondence, or propositions-as-types paradigm, provides a canonical logical foundation for functional programming [42]. It identifies types with logical propositions, programs with proofs, and computation with proof normalisation. It was natural to ask for a similar account of concurrent programming, and this question was brought into focus by the discovery of linear logic [24] and Girard’s explicit suggestion that it should have some connection with concurrent computation. Several attempts were made to relate \(\pi \)-calculus processes to the proof nets of classical linear logic [1, 8], and to relate CCS-like processes to the \(*\)-autonomous categories that provide semantics for classical linear logic [2]. However, this work did not result in a convincing propositions-as-types framework for concurrency, and did not continue beyond the 1990s.
Fig. 1.

Cyclic scheduler

Meanwhile, Honda et al. [26, 27, 38] developed session types as a formalism for statically checking that messages have the correct types and sequence according to a communication protocol. Research on session types developed and matured over several years, eventually inspiring Caires and Pfenning [12] to discover a Curry-Howard correspondence between dual intuitionistic linear logic [7] and a form of \(\pi \)-calculus with session types [38]. Wadler [41] subsequently gave an alternative formulation based on classical linear logic, and related it to existing work on session types for functional languages [23]. The Caires-Pfenning approach has been widely accepted as a propositions-as-types theory of concurrent programming, as well as providing a logical foundation for session types.

Caires and Pfenning’s type system guarantees deadlock-freedom by forbidding cyclic process structures. It provides a logical foundation for deadlock-free session processes, complementing previous approaches to deadlock-freedom in session type systems [9, 15, 21, 22]. The logical approach to session types has been extended in many ways, including features such as dependent types [39], failures and non-determinism [11], sharing and races [6]. All this work relies on the acyclicity condition. However, rejecting cyclic process structures is unnecessarily strict: they are a necessary, but not sufficient, condition for the existence of deadlocked communication operations. As we will show in Example 1 (Fig. 1), there are deadlock-free processes that can naturally be implemented in a cyclic way, but are rejected by Caires and Pfenning’s type system.

Our contribution is to define a new logic, priority-based linear logic (PLL), and formulate it as a type system for priority-based CP (PCP), which is a more expressive class of processes than Wadler’s CP [41]. This is the first Curry-Howard correspondence that allows cyclic interconnected processes, while still ensuring deadlock-freedom. The key idea is that PLL includes conditions on inter-channel dependencies based on Kobayashi’s type systems [29, 30, 32]. Our work can be viewed in three ways: (i) as a new linear logic in which cyclic proof structures can be derived; (ii) as an extension of Caires-Pfenning type systems so that they accept more processes, while maintaining the strong logical foundation; (iii) as a logical foundation for Kobayashi-style type systems.

An example of a deadlock-free cyclic process is Milner’s well-known scheduler [35], described in the following Example 1.

Example 1

(Cyclic Scheduler, Fig. 1). A set of agents \(A_0,..., A_{n-1}\), for \(n>1\), is scheduled to perform a certain task in cyclic order, starting with agent \(A_0\). For all \(i\in \{1,..., n-1\}\), agent \(A_i\) sends the result of computation to a collector process \(P_i\), before transmitting further data to agent Open image in new window . At the end of the round, \(A_0\) sends the final result to \(P_0\). Here we define a finite version of Milner’s scheduler, which executes one round of communication.

Prefix \({c}_{0} [{\mathbf {n}}_{0}]\) denotes an output on \({c}_{0}\), and \({d}_{0} ({{x}_{0}})\) an input on \({d}_{0}\). For now, let \(\mathbf {m}\) and \(\mathbf {n}\) denote data. Process \(\mathsf {close}_{i}\) closes the channels used by \(A_i\): the details of this closure are irrelevant here (however, they are as in processes Q and R in Example 2). Process \(Q_i\) uses the message received from \(A_i\), in internal computation. The construct \(({\varvec{\nu }} ab)\) creates two channel endpoints a and b and binds them together. The system Sched is deadlock-free because \(A_1,...,A_{n-1}\) each wait for a message from the previous \(A_i\) before sending, and \(A_0\) sends the initial message.

Sched is not typable in the original type systems by Caires-Pfenning and Wadler. To do that, it would be necessary to break \(A_0\) into two parallel agents \(A_0' \ \triangleq \ {c}_{0} [{\mathbf {n}}_{0}].\mathsf {close}_{{c}_{0}}\) and \(A_0'' \ \triangleq \ {d}_{0} ({{x}_{0}}).{a}_{0}[{\mathbf {m}}_{0}].\mathsf {close}_{{d}_{0},{a}_{0}}\). This changes the design of the system, yielding a different one. Moreover, if the scheduler continues into a second round of communication, this redesign is not possible because of the potential dependency from the input on \({d}_{0}\) to the next output on \({c}_{0}\). However, Sched is typable in PCP; we will show the type assignment at the end of Sect. 2.

There is a natural question at this point: given that the cyclic scheduler is deadlock-free, is it possible to encode its semantics in CP , thus eliminating the need for PCP ? It is possible to define a centralised agent A that communicates with all the collectors \(P_i\), resulting in a system that is semantically equivalent to our Sched. However, such an encoding has a global character, and changes the structure of the overall system from distributed to centralised. In programming terms, it corresponds to changing the software design, as we pointed out in Example 1, and ultimately the software architecture, which is not always desirable or even feasible. The aim of PCP is to generalise CP so that deadlock-free processes can be constructed with their natural structure. We would want any encoding of PCP into CP to be structure-preserving, which would mean translating the \(\small \textsc {Cycle}\) rule (given in Fig. 2) homomorphically; this is clearly impossible.

Contributions and Structure of the Paper. In Sect. 2 we define priority-based linear logic (PLL), which extends classical linear logic (CLL) with priorities attached to propositions. These priorities are based on Kobayashi’s annotations for deadlock freedom [32]. By following the propositions-as-types paradigm, we define a term assignment for PLL proofs, resulting in priority-based classical processes (PCP), which extends Wadler’s CP [41] with \(\small \textsc {Mix}\) and \(\small \textsc {Cycle}\) rules (Fig. 2). In Sect. 3 we define an operational semantics for PCP. In Sect. 4 we prove \(\small \textsc {Cycle}\)-elimination (Theorem 1) for PLL, analogous to the standard \(\small \textsc {Cut}\)-elimination theorem for CLL. Consequently, the results for PCP are subject reduction (Theorem 2), top-level deadlock-freedom (Theorem 3), and full deadlock-freedom for closed processes (Theorem 4). In Sect. 5 we discuss related work and conclude the paper.

2 PCP: Classical Processes with Mix and Cycle

Priority-based CP (PCP) follows the style of Wadler’s Classical Processes (CP) [41], with details inspired by Carbone et al. [14] and Caires and Pérez [11].

Types. We start with types, which are based on CLL propositions. Let AB range over types, given in Definition 1. Let \(\mathsf {o}, \kappa \in \mathbb {N}\cup \{\omega \}\) range over priorities, which are used to annotate types. Let \(\omega \) be a special element such that \(\mathsf {o}<\omega \) for all \(\mathsf {o}\in \mathbb {N}\). Often, we will omit \(\omega \). We will explain priorities later in this section.

Definition 1

(Types). Types (AB) are given by:

\(\mathbf{\bot }^\mathsf {o}\) and \(\mathbf{1}^\mathsf {o}\) are associated with channel endpoints that are ready to be closed. \(A \, {\otimes }^{\mathsf {o}}\, B\) (respectively, Open image in new window ) is associated with a channel endpoint that first outputs (respectively, inputs) a channel of type A and then proceeds as B. \(\oplus ^{\mathsf {o}}\{{l}_i:{A}_i\}_{i\in I}\) is associated with a channel endpoint over which we can select a label from \(\{l_i\}_{i\in I}\), and proceed as \(A_i\). Dually, Open image in new window is associated with a channel endpoint that can offer a set of labelled types. Open image in new window types a collection of clients requesting A. Dually, Open image in new window types a server repeatedly accepting A.

Duality on types is total and is given in Definition 2. It preserves priorities of types.

Definition 2

(Duality). The duality function \((\cdot )^\bot \) on types is given by:

Processes. Let PQ range over processes, given in Definition 3. Let xy range over channel endpoints, and \(\mathbf {m}, \mathbf {n}\) over channel endpoints of type either \(\mathbf{\bot }^\mathsf {o}\) or \(\mathbf{1}^\mathsf {o}\).

Definition 3

(Processes). Processes (PQ) are given by:

Process \(x[y].P\) (respectively, \(x({y}).P\)) outputs (respectively, inputs) y on channel endpoint x, and proceeds as P. Process \(x\triangleleft {l_j}.P\) uses x to select \(l_j\) from a labelled choice process, typically being \(x\triangleright \{{l}_i:P_i\}_{i\in I}\), and triggers \(P_j\); labels indexed by the finite set I are pairwise distinct. Process \({x}\!\rightarrow \!{y}^{A}\) forwards communications from x to y, the latter having type A. Processes also include the inaction process \({\varvec{0}}\), the parallel composition of P and Q, denoted \(P \mathord {\;\varvec{|}\;}Q\), and the double restriction constructor \(({\varvec{\nu }} {x}^{A}{y})P\): the intention is that x and y denote dual session channel endpoints in P, and A is the type of x. Processes \({x}[\,].{\varvec{0}}\) and \({x}().P\) are the empty output and empty input, respectively. They denote the closure of a session from the viewpoint of each of the two communicating participants.

Notions of bound/free names in processes are standard; we write \(\mathtt{{f}n}(P)\) to denote the set of free names of P. Also, we write Open image in new window to denote the (capture-avoiding) substitution of x for the free occurrences of z in P. Finally, we let \(\tilde{x}\), which is different from x, denote a sequence \(x_1, \ldots ,x_n\) for \(n>0\).

Typing Rules. Typing contexts, ranged over by \(\varGamma , \varDelta , \varTheta \), are sets of typing assumptions \(x\! :\!A\). We write \(\varGamma , \varDelta \) for union, requiring the contexts to be disjoint. A typing judgement \(P \vdash \varGamma \) means “process P is well typed using context \(\varGamma \)”.

Before presenting the typing rules, we need some auxiliary definitions. Our priorities are based on the annotations used by Kobayashi [32], but simplified to single priorities à la Padovani [37]. They obey the following laws:
  1. (i)

    An action of priority \(\mathsf {o}\) must be prefixed only by actions of priorities strictly smaller than \(\mathsf {o}\).

  2. (ii)

    Communication requires equal priorities for the complementary actions.


Definition 4

(Priority). The priority function \(\mathsf {pr}_{}(\cdot )\) on types is given by:

Definition 5

(Lift). Let \(t \in \mathbb {N}\). The lift operator \(\mathop {\uparrow ^{t}}{}(\cdot )\) on types is given by:
We assume \(\omega + t = \omega \) for all \(t \in \mathbb {N}\).

The operator \(\mathop {\uparrow ^{t}}\) is extended component-wise to typing contexts: \(\mathop {\uparrow ^{t}}\varGamma \).

The typing rules are given in Fig. 2. Open image in new window states that the forwarding process \({x}\!\rightarrow \!{y}^{A}\) is well typed if x and y have dual types, respectively \({A}^{\perp }\) and A. Open image in new window types the parallel composition of two processes P and Q in the union of their disjoint typing contexts. Open image in new window is our key typing rule; it states that the restriction process is well typed, if the endpoints x and y have dual types, respectively A and \({A}^{\perp }\). By Definition 2, A and \({A}^{\perp }\) also have the same priorities, enforcing law (ii) above. In classical logic this rule would be unsound, but in PLL it allows deadlock-free cycles. Rule \(\emptyset \) states that inaction is well typed in the empty context. Rules \(\mathbf{1}\) and \(\bot \) type channel closure actions from the viewpoint of each participant. Rule Open image in new window (respectively \(\otimes \)) types an input process \(x({y}).P\) (respectively, output process \(x[y].P\)), with y bound and x of type Open image in new window (respectively, \(A \, {\otimes }^{\mathsf {o}}\, B\)). The priority \(\mathsf {o}\) is strictly smaller than any priorities in the continuation process P, enforcing law (i) above. This is captured by \(\mathsf {o}< \mathsf {pr}_{}(\varGamma )\) in the premises of both rules, abbreviating “for all \(z\in \mathtt{{d}om}(\varGamma ), \mathsf {o}<\mathsf {pr}_{}(\varGamma (z))\)”. Rules Open image in new window and \(\oplus \) type external and internal choice, respectively, and follow the previous two rules. Rule Open image in new window types a server and states that if P communicates along y following protocol A, then Open image in new window communicates along x following protocol Open image in new window . The three remaining rules type different numbers of clients. Rule Open image in new window is for a single client: if P communicates along y following A, then Open image in new window communicates along x following Open image in new window . Rule Open image in new window is for no client: if P does not communicate along any channel following A, then it may be regarded as communicating along x following Open image in new window , for some priority \(\mathsf {o}\). Rule Open image in new window is for multiple clients: if P communicates along y following Open image in new window , and z following protocol Open image in new window , then Open image in new window communicates along a single channel x following Open image in new window , where \(\mathsf {o}\leqslant \mathsf {\kappa }\) and \(\mathsf {o}\leqslant \mathsf {\kappa }'\). The last two conditions are necessary to deal with some cases in the proof of \(\small \textsc {Cycle}\)-elimination (Theorem  1).
Fig. 2.

Typing rules for PCP.

Lifting preserves typability, by an easy induction on typing derivations.

Lemma 1

If \(P\vdash \varGamma \) then \(P\vdash \mathop {\uparrow ^{t}}{\varGamma }\).

We will use this result in the form of an admissible rule:    Open image in new window

The Design of Open image in new window We have included \(\small \textsc {Mix}\) and \(\small \textsc {Cycle}\), which allow derivation of both the standard \(\small \textsc {Cut}\) and the \(\small \textsc {Multicut}\) by Abramsky et al. [2].
Conversely, \(\small \textsc {Mix}\) is the nullary case of \(\small \textsc {Multicut}\), and \(\small \textsc {Cycle}\) can be derived from \(\small \textsc {Ax}\) and \(\small \textsc {Multicut}\):
Having included \(\small \textsc {Mix}\), we choose \(\small \textsc {Cycle}\) instead of \(\small \textsc {Multicut}\), as \(\small \textsc {Cycle}\) is more primitive.
In the presence of \(\small \textsc {Mix}\) and \(\small \textsc {Cycle}\), there is an isomorphism between \(A\otimes B\) and Open image in new window in CLL. Both Open image in new window and Open image in new window , are derivable, where Open image in new window in CLL. Equivalently, both Open image in new window and Open image in new window are derivable. For simplicity, let \(\mathsf {pr}_{}(A) = \mathsf {pr}_{}(B) = \omega \); by duality also \(\mathsf {pr}_{}({A}^{\perp }) = \mathsf {pr}_{}({B}^{\perp }) = \omega \).

The above derivations without priorities show the isomorphism between \(A\otimes B\) and Open image in new window in CLL, which does not hold in our PLL, in particular as \(\mathsf {o}_1 \ne \mathsf {o}_2\). The distinction between \(\otimes \) and Open image in new window , preserves the distinction between output and input in the term assignment. However, to simplify derivations, both typing rules (Fig. 2) have the same form. The usual tensor rule, where there are two separate derivations in the premise rather than just one, is derivable by using \(\small \textsc {Mix}\).

Our type system performs priority-checking. Priorities can be inferred, as in Kobayashi’s type system [32] and the tool TyPiCal [28]. We have opted for priority checking over priority inference, as the presentation is more elegant.

The following two examples illustrate the use of priorities. We first establish the structure of the typing derivation, then calculate the priorities. We conclude the section by showing the typing for the cyclic scheduler from Sect. 1.

Example 2

(Cyclic process: deadlock-free). Consider the following process
$$\begin{aligned} P\ \triangleq \ ({\varvec{\nu }} x_1y_1)({\varvec{\nu }} x_2y_2) \big [ x_1({v}).x_2({w}).R \mathord {\;\varvec{|}\;}y_1[\mathbf {n}].y_2[\mathbf {n}'].Q \big ] \end{aligned}$$
where \(R\ \triangleq \ {x_1}().{{v}().{{x_2}().{{w}().{\varvec{0}}}}}\) and \(Q\ \triangleq \ {y_1}[\,].{\varvec{0}} \mathord {\;\varvec{|}\;}{\mathbf {n}}[\,].{\varvec{0}}\mathord {\;\varvec{|}\;}{y_2}[\,].{\varvec{0}} \mathord {\;\varvec{|}\;}{\mathbf {n}'}[\,].{\varvec{0}}\). First, we show the typing derivation for the left-hand side of the parallel, \(x_1({v}).x_2({w}).R\):
Now, the typing derivation for the right-hand side of the parallel, \(y_1[\mathbf {n}].y_2[\mathbf {n}'].Q\), and recall that \(\mathsf {\kappa }_4< \mathsf {\kappa }_3<\mathsf {\kappa }_2 < \mathsf {\kappa }_1\):
Finally, the typing derivation for process P is as follows:
The system of equations
can be solved by the assignment \(\mathsf {o}_1 = \mathsf {o}_3 = 1\) and \(\mathsf {o}_2 = \mathsf {o}_4 = 0\).

Example 3

(Cyclic process: deadlocked!). Now consider the process
$$\begin{aligned} P' = ({\varvec{\nu }} x_1y_1)({\varvec{\nu }} x_2y_2) \big [ x_1({v}).x_2({w}).R \mathord {\;\varvec{|}\;}y_2[\mathbf {n}'].y_1[\mathbf {n}].Q \big ] \end{aligned}$$
where \(R = {x_1}().{{v}().{{x_2}().{{w}().{\varvec{0}}}}}\) and \(Q = {y_1}[\,].{\varvec{0}} \mathord {\;\varvec{|}\;}{\mathbf {n}}[\,].{\varvec{0}}\mathord {\;\varvec{|}\;}{y_2}[\,].{\varvec{0}} \mathord {\;\varvec{|}\;}{\mathbf {n}'}[\,].{\varvec{0}}\). Notice that the order of actions on channels \(y_1\) and \(y_2\) is now swapped, thus causing a deadlock! If we tried to construct a typing derivation for process \(P'\), we would have for the right-hand side of the parallel the following:
Then, the system of equations
has no solution because it requires \(\mathsf {o}_2 <\mathsf {o}_3\) and \(\mathsf {o}_3 <\mathsf {o}_2\), which is impossible.
Example 1 continued (Cyclic Scheduler)
By applying the typing rules in Fig. 2 we can derive \(Sched \vdash \emptyset \), since it is a closed process, and assign the following types and priorities:
The priorities of types \(\mathbf{\bot }\) and \(\mathbf{1}\) could be easily assigned as Example 2. As the priority of \(d_{i+1}\) is \(2(i+1)-2 = 2i\), we can connect it to \(a_i\) with a \(\small \textsc {Cycle}\).

3 Operational Semantics of PCP

In this section we define structural equivalence, the principal \(\beta \)-reduction rules and commuting conversions. The detailed derivations can be found in [18].

We define structural equivalence to be the smallest congruence relation satisfying the following axioms. \(\small \textsc {SC-Ax-Swp}\) allows swapping channels in the forwarding process. \(\small \textsc {SC-Ax-Cycle}\) states that cycle applied to a forwarding process is equivalent to inaction. This allows elimination of unnecessary cycles. Axioms \(\small \textsc {SC-Mix-Nil}\), \(\small \textsc {SC-Mix-Comm}\) and \(\small \textsc {SC-Mix-Asc}\) state that parallel composition uses the inaction as the neutral element and is commutative and associative. \(\small \textsc {SC-Cycle-Ext}\) is the standard scope extrusion rule. \(\small \textsc {SC-Cycle-Swp}\) allows swapping channels and \(\small \textsc {SC-Cycle-Comm}\) states the commutativity of restriction1.
Fig. 3.

\(\beta \)-reduction for \(\otimes \) and Open image in new window .

The core of the operational semantics consists of \(\beta \)-reductions. In \(\pi \)-calculus terms these are communication steps; in logical terms they are \(\small \textsc {Cycle}\)-elimination steps. Open image in new window is given in Fig. 3 to illustrate priorities. It simplifies a cycle connecting x of type \(A\, {\otimes }^{\mathsf {o}}\, B\) and y of type Open image in new window , which corresponds to communication between an output on x and an input on y, respectively. Both actions have priority \(\mathsf {o}\), which is strictly smaller than any priorities in their typing contexts, respecting the fact that they are top-level prefixes. The remaining \(\beta \)-reductions are summarised below. \(\beta _{\small \textsc {AxCycle}}\) simplifies a \(\small \textsc {Cycle}\) involving an axiom. \(\beta _{\mathbf{1}\bot }\) closes and eliminates channels. Open image in new window , similarly to Open image in new window , simplifies a communication between a selection and a branching. Open image in new window simplifies a cycle between one server of type Open image in new window and one client of type Open image in new window . The last two rules differ in the number of clients involved: rule Open image in new window considers no clients, whether Open image in new window considers multiple clients.
Commuting conversions, following [12, 41], allow communication prefixes to be moved to the conclusion of a typing derivation, corresponding to pulling them out of the scope of \(\small \textsc {Cycle}\) rules. In order to account for the sequence of \(\small \textsc {Cycle}\)s, here we use \(\tilde{\cdot }\). Due to this movement, if a prefix on a channel endpoint x with priority \(\mathsf {o}\) is pulled out at top level, then to preserve priority conditions in the typing rules in Fig. 2, it is necessary to increase priorities of all actions after the prefix on x. This increase is achieved by using \(\mathop {\uparrow ^{\mathsf {o}+1}}(\cdot )\) in the typing contexts.
Finally, we give the following additional reduction rules: closure under structural equivalence, and two congruence rules, for restriction and for parallel.

4 Results for PLL and PCP

4.1 \(\small \textsc {Cycle}\)-Elimination for PLL

We start with results for \(\small \textsc {Cycle}\)-elimination for PLL; thus here we refer to AB as propositions, rather than types. The detailed proofs can be found in [18].

Definition 6

The degree function \(\partial ({\cdot })\) on propositions is defined by:
  • \(\partial ({\mathbf{1}^\mathsf {o}}) = \partial ({\mathbf{\bot }^\mathsf {o}}) = 1\)

  • Open image in new window

  • \( \partial ({{ \& ^{\mathsf {o}}\{{l}_i:{A}_i\}_{i\in I}}}) = \partial ({\oplus ^{\mathsf {o}}\{{l}_i:{A}_i\}_{i\in I}}) = \sum _{i\in I}\{\partial ({A_i}) \} +1\)

  • Open image in new window .

Definition 7

A \(\small \textsc {Maxicut}\) is a maximal sequence of \(\small \textsc {Mix}\) and \(\small \textsc {Cycle}\) rules, ending with a \(\small \textsc {Cycle}\) rule.

Maximality means that the rules applied immediately before a \(\small \textsc {Maxicut}\) are any rules in Fig. 2, other than \(\small \textsc {Mix}\) or \(\small \textsc {Cycle}\). The order in which \(\small \textsc {Mix}\) and \(\small \textsc {Cycle}\) rules are applied within a \(\small \textsc {Maxicut}\) is irrelevant. However, Proposition 1, which follows directly from structural equivalence (Sect. 3), allows us to simplify a \(\small \textsc {Maxicut}\).

Proposition 1

(Canonical Open image in new window ). Given an arbitrary \(\small \textsc {Maxicut}\), it is always possible to obtain from it a canonical \(\small \textsc {Maxicut}\) consisting of a sequence of only \(\small \textsc {Mix}\) rules followed by a sequence of only \(\small \textsc {Cycle}\) rules.

Definition 8

A single-\(\small \textsc {Mix}\) \(\small \textsc {Maxicut}\) contains only one \(\small \textsc {Mix}\) rule.

\(A_1,\ldots ,A_n, A\) are \(\small \textsc {Maxicut}\) propositions if they are eliminated by a \(\small \textsc {Maxicut}\).

The degree of a sequence of \(\small \textsc {Cycle}\)s is the sum of the degrees of the eliminated propositions.

The degree of a \(\small \textsc {Maxicut}\) is the sum of the degrees of the \(\small \textsc {Cycle}\)s in it.

The degree of a proof \(\pi \), \(d(\pi )\), is the sup of the degrees of its \(\small \textsc {Maxicut}\)s, implying \(d(\pi )= 0\) if and only if proof \(\pi \) has no \(\small \textsc {Cycle}\)s.

The height of a proof \(\pi \), \(h(\pi )\), is the height of its tree, and it is defined as \(h(\pi )= {\mathrm {sup}\big (h(\pi _i)\big )}_{i\in I}+1\), where \(\{\pi _i\}_{i\in I}\) are the subproofs of \(\pi \).

\(\small \textsc {Maxicut}\) has some similarities with the derived \(\small \textsc {Multicut}\): it generalises \(\small \textsc {Multicut}\) in the number of \(\small \textsc {Mix}\)es, and a single-\(\small \textsc {Mix}\) \(\small \textsc {Maxicut}\) is an occurrence of \(\small \textsc {Multicut}\).

The core of \(\small \textsc {Cycle}\)-elimination for our PLL, as for \(\small \textsc {Cut}\)-elimination for CLL [10, 25], is the Principal Lemma (Lemma 3), which eliminates a \(\small \textsc {Cycle}\) by either (i) replacing it with another \(\small \textsc {Cycle}\) on simpler propositions, or (ii) pushing it further up the proof tree. Item (i) corresponds to (the logical part of) \(\beta \)-reductions (Sect. 3); and (ii) corresponds to (the logical part of) commuting conversions (Sect. 3).

Exceptionally, Open image in new window reduces the original proof in a way that neither (i) nor (ii) are respected. In order to cope with this case, we introduce Lemma 2, which is inspired by Lemma B.1.3 in Bräuner [10], and adapted to our PLL. Lemma 2 allows us to reduce the degree of a proof ending with a single-\(\small \textsc {Mix}\) \(\small \textsc {Maxicut}\) and having the same degree as the whole proof, and where the last rule applied on the left hand-side immediate subproof is Open image in new window . Let [n] denote the set \(\{1,\ldots ,n\}\).

Lemma 2

(Inspired by B.1.3 in Bräuner [10]). Let \(\tau \) be a proof of the following form, ending with a single-\(\small \textsc {Mix}\) \(\small \textsc {Maxicut}\):
where \(d(\pi )<d(\tau )\) and \(d(\pi ') <d(\tau )\). Then, there is a proof \(\tau '\) of Open image in new window such that \(d(\tau ') < d(\tau )\).


Induction on \(h(\pi ')\), with a case-analysis on the last rule applied in \(\pi '\).    \(\square \)

Lemma 3

(The Principal Lemma). Let \(\tau \) be a proof of \(~\vdash \varGamma \), ending with a canonical \(\small \textsc {Maxicut}\):
such that for all \(i \in [m]\), \(d(\pi _i) < d(\tau )\). Then there is a proof \(\tau '\) of \(~\vdash \mathop {\uparrow ^{t}}\varGamma \), for some \(t\geqslant 0\), such that \(d(\tau ') < d(\tau )\).


The proof is by induction on \(\sum _{i\in [m]} h(\pi _i)\). Let \(r_i\) be the last rule applied in \(\pi _i\), for \(i \in [m]\) and let \(C_{r_i}\) be the proposition introduced by \(r_i\). Consider the proposition with the smallest priority. If the proposition is not unique, just pick one. Let this proposition be \(C_{r_k}\). Then, \(\pi _k\) is the following proof:   Open image in new window

We proceed by cases on \(\pi _k\).

\(r_k\) is \(\otimes \) on one of the \(\small \textsc {Maxicut}\) propositions \(A_1,\ldots ,A_n, A\). Without loss of generality, suppose \(r_k\) is applied on A, meaning \(A = E\, {\otimes }^{\mathsf {o}}\, F\) for some E and F and \(\mathsf {o}\geqslant 0\). By \(\otimes \) rule in Fig. 2, \(\mathsf {o}< \mathsf {pr}_{}(\varGamma ')\). Since A is a \(\small \textsc {Maxicut}\) proposition, by Definition 2, Open image in new window . Since \(\mathsf {o}<\mathsf {pr}_{}(\varGamma ')\) and \(\mathsf {pr}_{}({A}^{\perp }) = \mathsf {o}\), it must be that \({A}^{\perp }\) is in another proof, say \(\pi _h\):     Open image in new window

Consider the case where \(r_h\) is a multiplicative, additive, exponential or \(\mathbf{\bot }\) rule in Fig. 2. Suppose \(r_h\) is applied on \(C_{r_h}\) which is not \({A}^{\perp }\). All the mentioned rules require Open image in new window , implying Open image in new window . This contradicts the fact that \(\mathsf {o}\) is the smallest priority. Hence, \(r_h\) must be a Open image in new window introducing \({A}^{\perp }\).

We construct proof \(\tau _A\) ending with a single-\(\small \textsc {Mix}\) \(\small \textsc {Maxicut}\) applied on at least A:
Then, by structural equivalence, we can rewrite \(\tau \) in terms of \(\tau _A\). By applying Open image in new window on \(\tau _A\) (only considering the logical part), we obtain a proof \(\tau '_A\) such that \(d(\tau '_A) < d(\tau _A) \le d(\tau )\), because \(\partial ({E}) +\partial ({F}) < \partial ({E \, {\otimes }^{\mathsf {o}}\, F})\). We can then construct \(\tau '\) by substituting \(\tau '_A\) for \(\tau _A\) in \(\tau \), which concludes this case.
\(r_k\) is Open image in new window on one of the \(\small \textsc {Maxicut}\) propositions \(A_1,\ldots ,A_n, A\). Without loss of generality, suppose \(r_k\) introduces A, implying that Open image in new window for some \(A'\) and \(\mathsf {o}\geqslant 0\). Then \(\pi _k\) is the following proof:

where Open image in new window . Since A is a \(\small \textsc {Maxicut}\) proposition, by duality Open image in new window . Since \(\mathsf {o}<\mathsf {pr}_{}(\varGamma ')\) and \(\mathsf {pr}_{}({A}^{\perp }) = \mathsf {o}\), it must be that \({A}^{\perp }\) is in another proof. Let it be \(\pi _h\) for \(h\in [m]\) and \(h\ne k\). Then we apply Lemma 2 to \(\pi _k\) and \(\pi _h\), obtaining a proof which we use to construct \(\tau '\), as we did in the previous case.    \(\square \)

Lemma 4

Given a proof \(\tau \) of \(\ \vdash \varGamma \), such that \(d(\tau )> 0\), then for some \(t\geqslant 0\) there is a proof \(\tau '\) of \(\ \vdash \mathop {\uparrow ^{t}}\varGamma \) such that \(d(\tau ') < d(\tau )\).


By induction on \(h(\tau )\). We have the following cases.

− If \(\tau \) ends in a \(\small \textsc {Maxicut}\) whose degree is the same as the degree of \(\tau \):
we can apply the induction hypothesis to the subproofs of \(\tau \) right before the last \(\small \textsc {Mix}\) preceding the sequence of \(\small \textsc {Cycle}\). This allows us to reduce their degrees to become smaller than \(d(\tau )\). Then we use Lemma 3.

− Otherwise, by using the inductive hypothesis on the immediate subproofs to reduce their degree, we also reduce the degree of the whole proof.    \(\square \)

Theorem 1

( Open image in new window -Elimination). Given any proof of \(\ \vdash \varGamma \), we can construct a \(\small \textsc {Cycle}\)-free proof of \(\ \vdash \mathop {\uparrow ^{t}}\varGamma \), for some \(t\geqslant 0\).


Iteration on Lemma 4.   \(\square \)

\(\small \textsc {Cycle}\)-elimination increases the priorities of the propositions in \(\varGamma \). This is solely due to the (logical part of) our commuting conversions in Sect. 3.

4.2 Deadlock-Freedom for PCP

Theorem 2

(Subject Reduction). If \(P\vdash \varGamma \) and \(P\longrightarrow Q\), then \(Q\vdash \mathop {\uparrow ^{t}}\varGamma \), for some \(t\geqslant 0\).


Follows from the \(\beta \)-reductions and commuting conversions in Sect. 3.   \(\square \)

Definition 9

A process is a \(\small \textsc {Cycle}\) if it is of the form \(({\varvec{\nu }} {x}^{A}{y}) P\).

Theorem 3

(Top-Level Deadlock-Freedom). If \(P\vdash \varGamma \) and P is a \(\small \textsc {Cycle}\), then there is some Q such that \(P\longrightarrow ^*Q\) and Q is not a \(\small \textsc {Cycle}\).


The interpretation of Lemma 3 for PCP is that either (i) a top-level communication occurs, corresponding to a \(\beta \)-reduction, or (ii) commuting conversions are used to push \(\small \textsc {Cycle}\) further inwards in a process. Consequently, iterating Lemma 3 results in eliminating top-level \(\small \textsc {Cycle}\)s.    \(\square \)

Eliminating all \(\small \textsc {Cycle}\)s, as specified by Theorem 1, would correspond to a semantics in which reduction occurs under prefixes, as discussed by Wadler [41]. In order to achieve this, we would need to introduce additional congruence rules, such as:
and similarly for other actions. Reductions of this kind are not present in the \(\pi \)-calculus, and we also omit them in our framework.

However, we can eliminate all \(\small \textsc {Cycle}\)s in a proof of \(\vdash \emptyset \), corresponding to full deadlock-freedom for closed processes. Kobayashi’s type system [32] satisfies the same property.

Theorem 4

(Deadlock-Freedom for Closed Processes). If \(P\vdash \emptyset \), then either \(P\equiv {\varvec{0}}\) or there is Q such that \(P\longrightarrow Q\).


This follows from Theorems 2 and 3, because if \(Q\vdash \emptyset \) and Q is not a \(\small \textsc {Cycle}\) then Q must be a parallel composition of \({\varvec{0}}\) processes.   \(\square \)

5 Related Work and Conclusion

\(\small \textsc {Cycle}\) and \(\small \textsc {Multicut}\) rules were explored by Abramsky et al. [2, 3, 4] in the context of \(*\)-autonomous categories. That work is not directly comparable with ours, as it only presented a typed semantics for CCS-like processes and did not give a type system for a language or a term assignment for a logical system. Atkey et al. [5] added a \(\small \textsc {Multicut}\) rule to CP, producing an isomorphism between \(\otimes \) and Open image in new window , but they did not consider deadlock-freedom.

In Kobayashi’s original type-theoretic approach to deadlock-freedom [29], priorities were abstract tags from a partially ordered set. In later work abstract tags were simplified to natural numbers, and priorities were replaced by pairs of obligations and capabilities [30, 32]. The latter change allows more processes to be typed, at the expense of a more complex type system. Padovani [36] adapted Kobayashi’s approach to session types, and later on he simplified it to a single priority for linear \(\pi \)-calculus [37]. Then, the single priority technique can be transferred to session types by the encoding of session types into linear types [16, 17, 19, 33]. For simplicity, we have opted for single priorities, as Padovani [37].

The first work on progress for session types, by Dezani-Ciancaglini et al. [15, 22], guaranteed the property by allowing only one active session at a time. Later work [21] introduced a partial order on channels in Kobayashi-style [29]. Bettini et al. [9] applied similar ideas to multiparty session types. The main difference with our work is that we associate priorities with individual communication operations, rather than with entire channels. Carbone et al. [13] proved that progress is a compositional form of lock-freedom and introduced a new technique for progress in session types by adopting Kobayashi’s type system and the encoding of session types [19]. Vieira and Vasconcelos [40] used single priorities and an abstract partial order in session types to guarantee deadlock-freedom.

The linear logic approach to deadlock-free session types started with Caires and Pfenning [12], based on dual intuitionistic linear logic, and was later formulated for classical linear logic by Wadler [41]. All subsequent work on linear logic and session types enforces deadlock-freedom by forbidding cyclic connections. In their original work, Caires and Pfenning commented that it would be interesting to compare process typability in their system with other approaches including Kobayashi’s and Dezani-Ciancaglini’s. However, we are aware of only one comparative study of the expressivity of type systems for deadlock-freedom, by Dardha and Pérez [20]. They compared Kobayashi-style typing and CLL typing, and proved that CLL corresponds to Kobayashi’s system with the restriction that only single cuts, not multicuts, are allowed.

In this paper, we have presented a new logic, priority-based linear logic (PLL), and a term assignment system, priority-based CP (PCP), that increase the expressivity of deadlock-free session type systems, by combining Caires and Pfenning’s linear logic-based approach and Kobayashi’s priority-based type system. The novel feature of PLL and PCP is \(\small \textsc {Cycle}\), which allows cyclic process structures to be formed if they do not violate ordering conditions on the priorities of prefixes. Following the propositions-as-types paradigm, we prove a \(\small \textsc {Cycle}\)-elimination theorem analogous to the standard \(\small \textsc {Cut}\)-elimination theorem. As a result of this theorem, we obtain deadlock-freedom for a class of \(\pi \)-calculus processes which is larger than the class typed by Caires and Pfenning. In particular, these are processes that typically share more than one channel in parallel.

There are two main directions for future work. First, develop a type system for a functional language, priority-based GV, and translate it into PCP, along the lines of Lindley and Morris’ [34] translation of GV [41] into CP. Second, extend PCP to allow recursion and sharing [6], in order to support more general concurrent programming, while maintaining deadlock-freedom, as well as termination, or typed behavioural equivalence.


  1. 1.

    Note that associativity of restriction is derived from \(\small \textsc {SC-Mix-Comm}\) and \(\small \textsc {SC-Cycle-Comm}\).



We are grateful for suggestions and feedback from the anonymous reviewers and colleagues: Wen Kokke, Sam Lindley, Roly Perera, Frank Pfenning, Carsten Schürmann and Philip Wadler.


  1. 1.
    Abramsky, S.: Proofs as processes. Theor. Comput. Sci. 135(1), 5–9 (1994)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Abramsky, S., Gay, S.J., Nagarajan, R.: Interaction categories and the foundations of typed concurrent programming. In: Broy, M. (ed.) Proceedings of the NATO Advanced Study Institute on Deductive Program Design, pp. 35–113 (1996)CrossRefGoogle Scholar
  3. 3.
    Abramsky, S., Gay, S., Nagarajan, R.: A type-theoretic approach to deadlock-freedom of asynchronous systems. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 295–320. Springer, Heidelberg (1997). Scholar
  4. 4.
    Abramsky, S., Gay, S.J., Nagarajan, R.: A specification structure for deadlock-freedom of synchronous processes. Theor. Comput. Sci. 222(1–2), 1–53 (1999)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Atkey, R., Lindley, S., Morris, J.G.: Conflation confers concurrency. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 32–55. Springer, Cham (2016). Scholar
  6. 6.
    Balzer, S., Pfenning, F.: Manifest sharing with session types. In: Proceedings of the ACM on Programming Languages, vol. 1(ICFP), pp. 37:1–37:29 (2017)CrossRefGoogle Scholar
  7. 7.
    Barber, A.: Dual intuitionistic linear logic. Technical report ECS-LFCS-96-347, University of Edinburgh (1996).
  8. 8.
    Bellin, G., Scott, P.J.: On the pi-calculus and linear logic. Theor. Comput. Sci. 135(1), 11–65 (1994)CrossRefGoogle Scholar
  9. 9.
    Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008). Scholar
  10. 10.
    Bräuner, T.: Introduction to linear logic. Technical report BRICS LS-96-6, Basic Research Institute in Computer Science, University of Aarhus (1996)Google Scholar
  11. 11.
    Caires, L., Pérez, J.A.: Linearity, control effects, and behavioral types. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 229–259. Springer, Heidelberg (2017). Scholar
  12. 12.
    Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010). Scholar
  13. 13.
    Carbone, M., Dardha, O., Montesi, F.: Progress as compositional lock-freedom. In: Kühn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 49–64. Springer, Heidelberg (2014). Scholar
  14. 14.
    Carbone, M., Lindley, S., Montesi, F., Schürmann, C., Wadler, P.: Coherence generalises duality: a logical explanation of multiparty session types. In: CONCUR. LIPIcs, vol. 59, pp. 33:1–33:15. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2016)Google Scholar
  15. 15.
    Coppo, M., Dezani-Ciancaglini, M., Yoshida, N.: Asynchronous session types and progress for object oriented languages. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 1–31. Springer, Heidelberg (2007). Scholar
  16. 16.
    Dardha, O.: Recursive session types revisited. In: BEAT. EPTCS, vol. 162, pp. 27–34 (2014)Google Scholar
  17. 17.
    Dardha, O.: Type Systems for Distributed Programs: Components and Sessions. Atlantis Studies in Computing, vol. 7. Atlantis Press, Paris (2016). Scholar
  18. 18.
    Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session typed processes. In: 21st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2018 (Extended Version).
  19. 19.
    Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: PPDP, pp. 139–150. ACM (2012)Google Scholar
  20. 20.
    Dardha, O., Pérez, J.A.: Comparing deadlock-free session typed processes. In: EXPRESS/SOS. EPTCS, vol. 190, pp. 1–15 (2015)Google Scholar
  21. 21.
    Dezani-Ciancaglini, M., de’Liguoro, U., Yoshida, N.: On progress for structured communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 257–275. Springer, Heidelberg (2008). Scholar
  22. 22.
    Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session types for object-oriented languages. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 328–352. Springer, Heidelberg (2006). Scholar
  23. 23.
    Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)zbMATHGoogle Scholar
  26. 26.
    Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993). Scholar
  27. 27.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998). Scholar
  28. 28.
    Kobayashi, N.: TyPiCal: type-based static analyzer for the pi-calculus.
  29. 29.
    Kobayashi, N.: A partially deadlock-free typed process calculus. ACM Trans. Program. Lang. Syst. 20(2), 436–482 (1998)CrossRefGoogle Scholar
  30. 30.
    Kobayashi, N.: A type system for lock-free processes. Inf. Comput. 177(2), 122–159 (2002)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Kobayashi, N.: Type systems for concurrent programs. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 439–453. Springer, Heidelberg (2003). Scholar
  32. 32.
    Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006). Scholar
  33. 33.
    Kobayashi, N.: Type systems for concurrent programs. Extended version of [31], Tohoku University (2007)Google Scholar
  34. 34.
    Lindley, S., Morris, J.G.: A semantics for propositions as sessions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 560–584. Springer, Heidelberg (2015). Scholar
  35. 35.
    Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  36. 36.
    Padovani, L.: From lock freedom to progress using session types. In: PLACES. EPTCS, vol. 137, pp. 3–19 (2013)Google Scholar
  37. 37.
    Padovani, L.: Deadlock and lock freedom in the linear \(\pi \)-Calculus. In: CSL-LICS, pp. 72:1–72:10. ACM (2014)Google Scholar
  38. 38.
    Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994). Scholar
  39. 39.
    Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP, pp. 161–172. ACM (2011)Google Scholar
  40. 40.
    Torres Vieira, H., Thudichum Vasconcelos, V.: Typing progress in communication-centred systems. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 236–250. Springer, Heidelberg (2013). Scholar
  41. 41.
    Wadler, P.: Propositions as sessions. In: ICFP, pp. 273–286. ACM (2012)Google Scholar
  42. 42.
    Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015)CrossRefGoogle Scholar

Copyright information

© The Author(s) 2018

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.School of Computing ScienceUniversity of GlasgowGlasgowUK

Personalised recommendations