Propositions in Linear Multirole Logic
as Multiparty Session Types
Hongwei Xi

Hanwen Wu

arXiv:1611.08888v1 [cs.PL] 27 Nov 2016

Boston University
{hwxi,hwwu}@cs.bu.edu

fun P() = let
val () =
channel_send(CH0, I1, 0, 1) // send to
val () =
channel_send(CH0, I2, 0, 1) // send to
val b0 = channel_recv(CH0, 1, 0) // recv
val () = channel_close(CH0) // close the
in b0 end (* end of [P] *)

Abstract
We identify multirole logic as a new form of logic and formalize linear multirole logic (LMRL) as a natural generalization of
classical linear logic (CLL). Among various meta-properties established for LMRL, we obtain one named multi-cut elimination stating that every cut between three (or more) sequents (as
a generalization of a cut between two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by
Gentzen. We also present a variant of π-calculus for multiparty
sessions that demonstrates a tight correspondence between process communication in this variant and multi-cut elimination in
LMRL, thus extending some recent results by Caires and Pfenning
(2010) and Wadler (2012), among others, along a similar line of
work.

1.

Q
Q
from Q
P-end of CH

fun Q() = let
val i1 =
channel_recv(CH1, 0, 1) // recv from P
val i2 =
channel_recv(CH1, 0, 1) // recv from P
val () =
channel_send(CH1, i1 < i2, 1, 0) // send to P
val () = channel_close(CH1) // close the Q-end of CH
in () end (* end of [Q] *)

Introduction

While the notion of multirole logic stems directly from studies
on multiparty sessions (Honda et al. 2008), we see it beneficial
to start with dyadic sessions (Honda 1993; Takeuchi et al. 1994).
In broad terms, a dyadic session is an interaction between two
concurrently running programs, and a session type is a form of
type for specifying sessions. As an example, let us assume that two
programs P and Q are connected with a bidirectional channel (that
is, a channel with two endpoints). From the perspective of P, the
channel may be specified by a term sequence of the following form:

Figure 1. Some pseudo code in ML-like syntax
where 0 (client) and 1 (server) refer to the two roles implemented
by P and Q, respectively. Given a type T and two roles i and
j, the term msg(i, j, T ) basically indicates a value of the type T
being transferred from a party implementing role i to another party
implementing role j. In particular, msg(i, j, T ) is interpreted as a
send (receive) operation by a party implementing role i ( j).
In Figure 1, we present some pseudo code showing a plausible way to implement the programs P and Q. Please note that the
functions P and Q, though written together here, can be written
in separate contexts. We use CH0 and CH1 for the two endpoints
of some channel CH (assumed to be available in the surrounding
context of the code) and I1 and I2 for two integers; the functions
channel send and channel recv are for sending and receiving
data via a given channel (endpoint), and channel close for closing one. In the following presentation, we use the name full channel
for a channel (like CH) and instead refer to each endpoint of a full
channel as a channel. For instance, CH0 (CH1) is a channel of role
0 (1), which is held by a party implementing role 0 (1).
Let us sketch a way to make the above pseudo code typecheck. Given an integer i and a session type S, let chan(i, S) be
the type for a channel of role i. We can assign the following type to
channel send:

snd(int) :: snd(int) :: rcv(bool) :: nil
which means that an integer is to be sent, another integer is to be
sent, a boolean is to be received, and finally the channel is to be
closed. Clearly, from the perspective of Q, the channel should be
specified by the following term sequence:
rcv(int) :: rcv(int) :: snd(bool) :: nil
which means precisely the dual of what the previous term sequence
does. We may think of P as a client who sends two integers to the
server Q and then receives from Q either true or false depending on
whether or not the first sent integer is less than the second one.
A simple but crucial observation is that the above two term
sequences can be unified as follows:
msg(0, 1, int) :: msg(0, 1, int) :: msg(1, 0, bool) :: nil

(!chan(i, msg(i, j, T ) :: S)  chan(i, S), int(i), int( j), T ) → 1
where i , j is assumed to hold, and int(i) and int( j) are singleton
types for integers equal to i and j, respectively, and T and S
stand for a type and a session type, respectively. Basically, this
type1 means that calling channel send on a channel of the type
1

Strictly speaking, this type should be referred to as a type schema as it
contains occurrences of meta-variables.

[Copyright notice will appear here once ’preprint’ option is removed.]

1

2018/3/1

chan(i, msg(i, j, T ) :: S), integer i, integer j and a value of the
type T returns a unit while changing the type of the channel to
chan(i, S). Clearly, chan is required to be a linear type constructor
for this to make sense. As can be expected, the type assigned to
channel recv should be of the following form:

As the channel is an endpoint of a full channel, the tagged value
should reach all of the other endpoints of the full channel.
• Assume i < R. Then any party holding a channel of type

chan(R, msg(i, j, T ) :: S) is supposed to receive on the channel
a tagged value in which the tag is j and the value is of type T .

(!chan( j, msg(i, j, T ) :: S)  chan( j, S), int(i), int( j)) → T

We may stipulate that any party should discard a tagged value
received on a channel of roles R if the attached tag does not belong
to R. If broadcasting from one endpoint of a full channel to the
others are built on top of point-to-point communication2 , then this
stipulation implies no need for actually sending a tagged value to
a channel of roles R whenever the attached tag does not belong to
R. With the stipulation, we have the following four scenarios for
interpreting msg(i, j, T ) based on a given set R of roles:

where i , j is assumed to hold. This type indicates that calling
channel recv on a channel of the type chan( j, msg(i, j, T ) :: S),
integer i and integer j returns a value of the type T while changing
the type of the channel to chan( j, S). As for channel close, it is
assigned the following type:
(chan(i, nil)) → 1

• Assume i ∈ R and j ∈ R. Then any party holding a chan-

indicating that calling channel close on a channel consumes the
channel (so that the channel is no longer available for use).
Assume that CHa and CHb are two full channels specified by a
session type S. The two endpoints CHa0 and CHa1 of CHa are given
the types chan(0, S) and chan(1, S), respectively. Similarly, the two
endpoints CHb0 and CHb1 of CHb are given the types chan(0, S) and
chan(1, S), respectively. If some party holds both CHa1 and CHb0 ,
then the party can link them together by performing a form of a
bidirectional forwarding that sends onto CHb0 each value received
on CHa1 and vice versa. After CHa1 and CHb0 are linked in such
a manner, CHa0 and CHb1 can be seen as the tw endpoints of a
full channel specified by S. It is well-known that bidirectional
forwarding between two matching channels (of types chan(0, S)
and chan(1, S) for some S) corresponds to cut-elimination in linear
logic (Caires and Pfenning 2010; Wadler 2012a).
Instead of two roles, let us assume the availability of three
roles 0, 1 and 2. One may be tempted to guess that the aforementioned bidirectional forwarding between two channels can be generalized to work in the case of three channels of types chan(0, S),
chan(1, S), and chan(2, S) for some S. Assume that CHa , CHb and
CHc are three full channels specified by a session type S. For each
x ∈ {a, b, c} and i ∈ {0, 1, 2}, CHix (as an endpoint of CH x ) is of
the type chan(i, S). If CHa2 , CHb1 and CHc0 are chosen to be linked
together so that each value received on one of them is sent onto another of them, then the other 6 endpoints CHa0 ,CHa1 , CHb0 ,CHb2 , CHc1
and CHa2 should form another full channel. This is certainly unexpected (if not unsound) as each full channel is assumed to have
only three endpoints: one for each of the three roles 0, 1 and 2. As
a consequence, we introduce multirole channels as follows.
Given a role i and a session type S, the type chan(i, S) for singlerole channels can be naturally transitioned into one of the form
chan(R, S) for multirole channels, where R stands for a set of roles.
In particular, chan(i, S) can be simply treated as chan({i}, S). For
notational convenience, we may simply write i for {i} from this
point on. Assume that there exists a fixed set of N roles ranging
from 0 to N − 1 for some natural number N ≥ 2. For each R,
we use R for the complement of R, which consists of all of the
natural numbers less than N that are not in R. In particular, ∅ refers
to the set {0, 1, . . . , N}. Each full channel CH specified by S may
have n endpoints CHRi that are assigned the types chan(Ri , S) for
i = 1, . . . , n, where R1 , . . . , Rn form a partition of ∅. If a value is
sent onto one of the endpoints, then this value is supposed to reach
all of the other endpoints. In other words, sending simply acts like
broadcasting.
We may refer to a channel as a channel of roles R if the channel
is assigned a type of the form chan(R, S). We have the following
two scenarios for interpreting msg(i, j, T ) based on a given set R:

nel of type chan(R, msg(i, j, T ) :: S) should ignore the term
msg(i, j, T ) as there is no other endpoint expecting to receive
a value tagged with j.
• Assume i < R and j < R. Then any party holding a chan-

nel of type chan(R, msg(i, j, T ) :: S) should ignore the term
msg(i, j, T ) as it is expected to neither send nor receive.
• Assume i ∈ R and j < R. Then any party holding a channel of

type chan(R, msg(i, j, T ) :: S) should send a value of type T (to
the only other endpoint expecting to receive such a value).
• Assume i < R and j ∈ R. Then any party holding a channel of

type chan(R, msg(i, j, T ) :: S) should receive a value of type T
(from the only other endpoint expecting to send such a value).
With the above interpretation, channel send can be assigned the
following type:
(!chan(R, msg(i, j, T ) :: S)  chan(R, S), int(i), int( j), T ) → 1
where i ∈ R and j < R is assumed; channel recv can be assigned
the following type:
(!chan(R, msg(i, j, T ) :: S)  chan(R, S), int(i), int( j)) → T
where i < R and j ∈ R is assumed. As for channel close, the
following type is assigned:
(chan(R, nil)) → 1
In addition, we need to introduce a function channel skip of the
following type:
(!chan(R, msg(i, j, T ) :: S)  chan(R, S)) → 1
where either i, j ∈ R or i, j < R is assumed. Note that channel skip
is really a proof function in the sense that it does nothing at runrime.
In the case where ∅ = {0, 1}, a party holding two channels of
types chan(0, S) and chan(1, S) can link them together by performing bidirectional forwarding (of values received on them) if each
channel is an endpoint of a distinct full channel. In the general case
where ∅ may contain more than 2 roles, a party holding n channels of types chan(Ri , S) for i = 1, . . . , n can link them together if
each channel is an endpoint of a distinct full channel and the role
sets R1 , . . . , Rn form a partition of ∅, that is, the following equality
holds:
R1 ] . . . ] Rn = ∅
where ] refers to the union of two disjoint sets. For instance, we
may have R1 = {0, 1}, R2 = {0, 2}, and R3 = {1, 2} in the case
where ∅ = {0, 1, 2}. The actual linking of such n channels can be
performed as follows:

• Assume i ∈ R. Then any party holding a channel of type

2

chan(R, msg(i, j, T ) :: S) is supposed to send onto the channel
a tagged value in which the tag is j and the value is of type T .

For instance, this is the case in an experimental implementation we did
where the underlying communication is based on shared memory.

2

2018/3/1

• Assume that a tagged value is received on one channel. Then a

for conjunction and disjunction:

type of the form chan(Ri , msg(p, q, T ) :: S) is assigned to the
channel originally, where p < Ri holds. Clearly, we have p ∈ Ri
and thus p ∈ R j for any role j that is not i (since R1 , . . . , Rn form
a partition of ∅), which means that the received tagged value can
be sent onto each of the remaining n − 1 channels.

A ` B, A A ` B, B
(conj-r)
A ` B, A ∧ B
A, A ` B
(conj-l-1)
A, A ∧ B ` B

A, A ` B A, B ` B
(disj-l)
A, A ∨ B ` B

It can be readily verified that the n distinct full channels involved
in such an act of linking form another full channel at the end.
As an example, let us assume the existence of 3 full channels
CHa , CHb and CHc that are all specified by S. For CHa , there
are two endpoints CHa0 and CHa00 that are of types chan(0, S) and
chan(00 , S), respectively, where 0 refers to the singleton set {0} and
00 the complement of {0}. For CHb , there are two endpoints CHb1
and CHb10 that are of types chan(1, S) and chan(10 , S), respectively.
For CHc , there are two endpoints CHc2 and CHc20 that are of types
chan(2, S) and chan(20 , S), respectively. The aforementioned act of
linking can be performed on the 3 endpoints CHa00 , CHb10 and CHc20 ,
resulting in the formation of a full channel consisting of the other 3
endpoints CHa0 , CHb1 and CHc3 .
While we made use of some linearly typed functions on channels to illustrate the notion of multirole, we do not attempt to
formally study such functions in this paper. Instead, we focus on
logic. Since the act of linking two matching channels can be given
an interpretation based on cut-elimination in intuitionistic linear
logic (Caires and Pfenning 2010) and classical linear logic (Wadler
2012a), we naturally expect that the act of linking n matching
channels (for n ≥ 2) can be interpreted similarly based on cutelimination in a linear logic of certain kind. We are able to form
linear multirole logic (LMRL) to serve this purpose precisely. For
long, studies on logics have been greatly influencing research on
programming languages. In the case of LMRL, we see a genuine
example that demonstrates the influence of the latter on the former.
The rest of the papers is organized as follows. We formulate
LMRL in Section 2, establishing various meta-properties for them.
We primarily focus on conjunctive LMRL (LMRL∧ ) while briefly
mentioning disjunctive LMRL (LMRL∨ ) as the dual of LMRLcon j.
We then present in Section 3 a process calculus πLMRL, which
can be seen as a typed variant of π-calculus. The session types in
πLMRL are just the formulas in LMRL and the reduction semantics
of πLMRL is directly based on cut-elimination in LMRL. Lastly,
we mention some closely related and conclude.
The primary contribution of the paper lies in the identification
of multirole logic as a new form of logic and the presented formalization of linear multirole logic (LMRL). We consider the formulation and proof of various meta-properties on LMRL a large part of
this contribution. In particular, we formulate a cut-rule for multiple
sequents in LMRL and prove its admissibility, naturally extending
the celebrated result of cut-elimination by Gentzen (Gentzen 1935).
Primarily for the purpose of comparing LMRL with intuitionistic
linear logic and classical linear logic, we also present a variant of
π-calculus for multiparty sessions that demonstrates a tight correspondence between process communication in this variant and
multi-cut elimination in LMRL, thus extending some recent results
on encoding session types as propositions in linear logic (Caires
and Pfenning 2010; Wadler 2012a).

2.

A, B ` B
(conj-l-2)
A, A ∧ B ` B

A ` B, A
(disj-r-1)
A ` B, A ∨ B

A ` B, B
(disj-r-2)
A ` B, A ∨ B

where A and B range over sequents (that are essentially sequences
of formulas). One possibility to explain this duality is to think of the
availability of two roles 0 and 1 such that the left side of a sequent
judgment (of the form A ` B) plays role 1 while the right side does
role 0. In addition, there are two logical connectives ∧0 and ∧1 ; ∧r
is given a conjunction-like interpretation by the side playing role
r and disjunction-like interpretation by the other side playing role
1 − r, where r ranges over 0 and 1. With this explanation, it seems
entirely natural for us to introduce more roles into classical logic.
Given a natural number N, we use RN for the set consisting of
all of the natural numbers less than N, and Rω for the set of natural
numbers. In addition, we use R for either RN (for some n ≥ 2) or
Rω , and may refer to each number in R as a role. Note that multirole
logic is parameterized over a chosen underlying set R of roles, and
we may use ∅ to refer to this set R. Given a subset R of some R, we
use R for the complement of R in R (assuming that this particular
R can be readily inferred from the context). Also, we use R1 ] R2
for the union of two disjoint sets R1 and R2 ..
Intuitively speaking, a conjunctive multirole logic is one in
which there is an underlying base set R of roles; for each r ∈ R,
there is a logical connective ∧r such that ∧r is given a conjunctionlike interpretation by a side playing role r and a disjunction-like interpretation otherwise. If we think of the universal quantifier ∀ as an
infinite form of conjunction, then what is said about ∧ can be readily applied to ∀ as well. In fact, additive, multiplicative, and exponential connectives in linear logic (Girard 1987) can all be treated
in a similar manner. Evidently, a disjunctive multirole logic can be
formulated dually (by giving ∧r a disjunction-like interpretation if
the side plays the role r and a conjunction-like interpretation otherwise). While there is certainly a version of multirole logic based on
classical logic, we solely focus on linear multirole logic (LMRL)
in this paper, which is based on classical linear logic.
Given a formula A and a set R of roles (which is a subset of
the underlying full set R), we write [A]R for an i-formula, which
is some sort of interpretation of A based on R. For instance, the
interpretation of ∧r based on R is conjunction-like if r ∈ R holds,
and it is disjunction-like otherwise. It is crucial to realize that
interpretations should be based on sets of roles rather than just
individual roles. In other words, one side is allowed to play multiple
roles simultaneously.
A sequent Γ in multirole logic is a sequence of i-formulas, and
such a sequent is inherently many-sided as each R appearing in
Γ represents just one side. Note that two identical i-formulas are
allowed to appear in one sequent. We use ∅ for the empty sequence
and (Γ, [A]R ) for any sequence that can be formed by inserting
[A]R into Γ (at any position). The parentheses in (Γ, [A]R ) may be
dropped if there is no risk of confusion. We use ` Γ for a judgment
meaning that Γ is derivable and may write (Γ1 ; . . . ; Γn ) ⇒ Γc for an
inference rule of the following form:

Linear Multirole Logic

While the first and foremost inspiration for multirole logic stems
from studies on multiparty session types in distributed programming, it seems natural in retrospective to (also) introduce multirole
logic by exploring (in terms of a notion referred to as role-based interpretation) the well-known duality between conjunction and disjunction in classical logic. For instance, in a two-sided presentation
of the classical sequent calculus (LK), we have the following rules

` Γ1

. . . ` Γn
` Γc

where ` Γ1 , . . . , ` Γn are the premisses of the rule and ` Γc the
conclusion.

3

2018/3/1

As can be readily expected, the cut-rule (for two sequents) in
(either conjunctive or disjunctive) LMRL is of the following form:

R1 ] . . . ] Rn = ∅
(Id∧ )
` [a]R1 , . . . , [a]Rn

Γ1 , [A]R Γ2 , [A]R
Γ1 , Γ2

r < R ` Γ, [A]R , [B]R
(⊗-neg)
` Γ, [A ⊗r B)]R

The cut-rule can be interpreted as some sort of communication
between two parties in distributed programming (Abramsky 1994a;
Bellin and Scott 1994b; Caires and Pfenning 2010; Wadler 2012a).
For communication between multiple parties, it is natural to seek a
generalization of the cut-rule that involve more than two sequents.
In conjunctive LMRL, the admissibility of the following cut-rule
(n-cut-conj) can be established for each n ≥ 1:
R1 ] . . . ] Rn = ∅

Γ1 , [A]R1

...

r∈R

r < R ` Γ, [A]R
(&-neg-l)
` Γ, [A &r B]R
r < R ` Γ, [B]R
(&-neg-r)
` Γ, [A &r B]R

Γn , [A]Rn

Γ1 , . . . , Γn

r∈R

In disjunctive LMRL, the admissibility of the following cut-rule
(n-cut-disj) can be established for each n ≥ 1:
R1 ] . . . ] Rn = ∅

Γ1 , [A]R1

...

r<R `Γ
(!-neg-weaken)
` Γ, [!r (A)]R

We will give explanation later on the case where n = 1. The case
where n = 2 is special as both of the conditions R1 ] R2 = ∅
R1 ] R2 = ∅ are equivalent to R1 and R2 being complement to each
other. Therefore, the rules 2-cut-conj and 2-cut-disj have the same
form as the standard cut-rule (for two sequents). If n is not 2, then
the rules n-cut-conj and n-cut-disj impose different pre-conditions
on the involved role sets R1 , . . . , Rn . Also, please note that the precondition on R1 , . . . , Rn as is imposed by the rule n-cut-conj is
identical to the requirement on R1 , . . . , Rn for linking n matching
channels of types chan(R1 , S), . . . , chan(R1 , S) stated in Section 1,
which naturally prompts one to guess the existence of a profound
relation between these two.

r < R ` Γ, [A]R
(!-neg-derelict)
` Γ, [!r (A)]R
r<R

r ∈ R x < Γ ` Γ, [A]R
(∀-pos)
` Γ, [∀r (λx.A)]R

Syntax

Figure 2. The inference rules for LMRL∧

A

::=

Note that there are one positive rule and one negative rule for
each ⊗r , and one positive rule and two negative rules for each &r ,
and one positive rule and one negative rule for each ∀r . Let us take
the rule (⊗-neg) as an example; the i-formula [A ⊗r B]R is referred
to as the major i-formula of the rule. Let us take the rule (⊗-pos)
as another example; the i-formula [A ⊗r B]R is referred to as the
major i-formula of the rule. The major i-formulas for the other rules
(excluding the rule (Id∧ )) should be clear as well. For the rule (Id∧ ),
each [a]Ri is referred to as a major i-formula.
We use |A| for the size of A, which is the number of connectives
contained in A We use D for a derivation tree and ht(D) for the
height of the tree. Also, we use D :: Γ for a derivation of Γ.

a | A1 ⊗r A2 | A1 &r A2 | !r (A) | ∀r (λx.A)

where a ranges over primitive ones. In CLL, ⊗ stands for the
multiplicative conjunction, & the additive conjunction, ! the ofcourse modality operator, and ∀ the universal quantifier. An iformula in LMRL is of the form [A]R , and a sequent Γ is a sequence
of i-formulas. We may write [?(A)]R to mean [!r (A)]R for some r <
R, and ?(Γ) to mean that each i-formula in Γ is of the form [?(A)]R .
Given a sequent Γ and an i-formula [A]R , we use (Γ, [A]R ) for a
sequent obtained from inserting [A]R into Γ (at any position). Given
two sequents Γ1 and Γ2 , we use (Γ1 , Γ2 ) for a sequent obtained
from merging Γ1 with Γ2 (in any kind of order). The parentheses
in (Γ, [A]R ) and (Γ1 , Γ2 ) may be dropped if there is no risk of
confusion. Given an i-formula [A]R , let us use {[A]R } for a sequent
consisting of only [A]R if A is not of the form !r (B) for r < R or
some repeated occurrences of [A]R otherwise (that is, if A is of the
form !r (B) for r < R).
2.2

` Γ, [!r (A)]R , [!r (A)]R
(!-neg-contract)
` Γ, [!r (A)]R

r < R ` Γ, [A{t/x}]R
(∀-neg)
` Γ, [∀r (λx.A)]R

We use t for (first-order) terms in LMRL, which are standard. For
each r ∈ R, there exist logical connectives ⊗r , &r , !r , and ∀r . The
formulas in LMRL are defined as follows:
formulas

` Γ, [A]R ` Γ, [B]R
(&-pos)
` Γ, [A &r B]R

r ∈ R ` ?(Γ), [A]R
(!-pos)
` ?(Γ), [!r (A)]R

Γn , [A]Rn

Γ1 , . . . , Γn

2.1

` Γ1 , [A]R ` Γ2 , [B]R
(⊗-pos)
` Γ1 , Γ2 , [A ⊗r B]R

Proposition 2.1 (Substitution). Given a sequent Γ, a variable x
and a term t, we use Γ{x/t} for the sequent obtained from replacing
each i-formula [A]R in Γ with [A{x/t}]R . Assume D1 :: Γ. Then we
can construct a derivation D2 of the sequent Γ{x/t}.
Proof. By structural induction on D1 .

LMRL∧ : Conjunctive LMRL

The inference rules for LMRL∧ are given in Figure 2. Note that ⊗r
is interpreted as ⊗ by a side playing the role r and O (the dual of ⊗
in CLL) by a side not playing the role r; &r is interpreted as & by
a side playing the role r and ⊕ (the dual of & in CLL) by a side not
playing the role r; !r is interpreted as ! by a side playing the role
r and ? (the dual of ! in CLL) by a side not play the role r; ∀r is
interpreted as ∀ (universal quantifier) by a side playing the role r
and ∃ (existential quantifier) by a side not playing the role r.



We may use D1 {x/t} for the D2 constructed in Proposition 2.1.
Lemma 2.2. The following rule is admissible in LMRL∧ :
(Γ, [A]∅ ) ⇒ Γ
Proof. By structural induction on the derivation of D :: (Γ, [A]∅ ).

4

2018/3/1

Note that Lemma 2.2 simply states the admissibility of the cutrule n-cut-conj for n = 1. So it actually makes sense to have a cut
involving only one sequent!

By the induction hypothesis on D11 and D21 , we obtain a
derivation:
D01 :: (Γ11 , Γ21 , [A1 ]R1 ∩R2 )

Lemma 2.3 (η-expansion). The following rule is admissible in
LMRL∧ :
() ⇒ [A]R1 , . . . , [A]Rn

By the induction hypothesis on D12 and D22 , we obtain a
derivation:
D02 :: (Γ12 , Γ22 , [A2 ]R1 ∩R2 )

where R1 ] . . . ] Rn = ∅.

By applying the rule (⊗-pos) to D01 and D02 , we obtain a derivation of the sequent (Γ, [A]R1 ∩R2 ).



Proof. By structural induction on A.

The next lemma is the most crucial one in this paper. While its
proof may seem rather involved, it should be readily accessible for
someone familiar with a standard cut-elimination proof.

Assume that A is of the form A1 &r A2 . We have three possibilities:
r ∈ R1 and r < R2 , or r < R1 and r ∈ R2 , or r ∈ R1 and r ∈ R2 .
• Assume r ∈ R1 and r < R2 . Then D1 is of the following form:

Lemma 2.4 (2-cut with spill). Assume that R1 and R2 are disjoint.
Then the following rule is admissible in LMRL∧ :

D11 :: (Γ1 , [A1 ]R1 )

` Γ1 , [A]R1

(Γ1 , [A]R1 ; Γ2 , [A]R2 ) ⇒ Γ1 , Γ2 , [A]R1 ∩R2

D2k :: (Γ2 , [Ak ]R2 )
` Γ2 , [A]R2
where the last applied rule in D2 is (&-neg-l) or (&-neg-r). By
induction hypothesis on D1k and D2k , we obtain a derivation:

(Γ1 , {[A]R1 }; Γ2 , {[A]R2 }) ⇒ Γ1 , Γ2 , [A]R1 ∩R2

D0k :: (Γ1 , Γ2 , [Ak ]R1 ∩R2 )

Note that the proof strategy we use is essentially adopted from
the one in a proof of cut-elimination for classical linear logic
(CLL) (Troelstra 1992). Assume D1 :: (Γ1 , {[A]R1 }) and D2 ::
(Γ2 , {[A]R2 }). We proceed by induction on |A| (the size of A) and
ht(D1 ) + ht(D2 ), lexicographically ordered. For brevity, we are
to focus only on the most interesting case where there is one
occurrence of [A]Ri in {[A]Ri } that is the major formula of the last
rule applied in Di , where i ranges over 1 and 2. For this case, we
have several subcases covering all the possible forms that A may
take.

By applying to D0k either (&-neg-l) or (&-neg-r), we obtain a
derivation of the sequent (Γ1 , Γ2 , [A]R1 ∩R2 ).
• Assume r < R1 and r ∈ R2 . Then this case is analogous to the
previous one.
• Assume r ∈ R1 and r ∈ R2 . Then Dk is of the following form
for each of the cases k = 1 and k = 2:
Dk1 :: (Γk1 , [A1 ]Rk ) Dk2 :: (Γk2 , [A2 ]Rk )
(&-pos)
` Γk , [A]Rk

Assume that A is primitive. Then it is a simple routine to verify
that the sequent ` (Γ1 , Γ2 , [A]R1 ∩R2 ) follows from an application of
the rule (Id∧ ).

By the induction hypothesis on D11 and D21 , we obtain a
derivation:
D01 :: (Γ11 , Γ21 , [A1 ]R1 ∩R2 )

Assume that A is of the form A1 ⊗r A2 . We have three possibilities:
r ∈ R1 and r < R2 , or r < R1 and r ∈ R2 , or r ∈ R1 and r ∈ R2 .

By the induction hypothesis on D12 and D22 , we obtain a
derivation:
D02 :: (Γ12 , Γ22 , [A2 ]R1 ∩R2 )

• Assume r ∈ R1 and r < R2 . Then D1 is of the following form:

D12 :: (Γ12 , [A2 ]R1 )

` Γ1 , [A]R1
and D2 is of the following form:
D21 :: (Γ2 , [A1 ]R2 , [A2 ]R2 )
` Γ2 , [A]R2

(&-pos)

and D2 is of the following form for k being either 1 or 2:

Proof. Due to the explicit presence of the three structural rules
(!-neg-weaken) (!-neg-derelict), and (!-neg-contract) in LMRL∧ ,
we need to prove a strengthened version of Lemma 2.4 stating that
the following rule is admissible in LMRL∧ :

D11 :: (Γ11 , [A1 ]R1 )

D12 :: (Γ1 , [A2 ]R1 )

By applying the rule (&-pos) to D01 and D02 , we obtain a derivation of the sequent (Γ1 , Γ2 , [A]R1 ∩R2 ).

(⊗-pos)

Assume that A is of the form !r (B). This is the most involved
subcase. We have three possibilities: r ∈ R1 and r < R2 , or r < R1
and r ∈ R2 , or r ∈ R1 and r ∈ R2 .

(⊗-neg)

• Assume r ∈ R1 and r < R2 . Then D1 is of the following form:

By the induction hypothesis on D11 and D21 , we have a derivation:
D011 :: (Γ11 , Γ2 , [A1 ]R1 ∩R2 , [A2 ]R2 )

D11 :: ?(Γ1 ), [B]R1
` ?(Γ1 ), [A]R1

By the induction hypothesis on D12 and D011 , we have a derivation:
D012 :: (Γ, [A1 ]R1 ∩R2 , [A2 ]R1 ∩R2 )

(!-pos)

There are the following three possibilities for D2 :
D2 is of the following form:
D21 :: Γ2 , {[A]R2 }

By applying the rule (⊗-neg) to D012 , we have a derivation of
the sequent (Γ, [A]R1 ∩R2 ).
• Assume r < R1 and r ∈ R2 . Then this case is analogous to the
previous one.
• Assume r ∈ R1 and r ∈ R2 . Then Dk is of the following form
for each of the cases k = 1 and k = 2:
Dk1 :: (Γk1 , [A1 ]Rk ) Dk2 :: (Γk2 , [A2 ]Rk )
(⊗-pos)
` Γk , [A]Rk

` Γ2 , {[A]R2 }

(!-neg-weaken)

We simply obtain a derivation of (Γ1 , Γ2 , [A]R1 ∩R2 ) by the
induction hypothesis on D1 and D21 .
D2 is of the following form:
D21 :: Γ2 , {[A]R2 }, [B]R
` Γ2 , {[A]R2 }
5

(!-neg-derelict)

2018/3/1

By the induction hypothesis on D1 and D21 , we obtain a
derivation:

Lemma 2.5 (2-cut). The following rule is admissible in LMRL∧ :
(Γ1 , [A]R ; Γ2 , [A]R ) ⇒ Γ1 , Γ2

D121 :: (Γ1 , Γ2 , [A]R1 ∩R2 , [B]R )

Lemma 2.5 is just a special case of Lemma 2.6 where n is 2.

By the induction hypothesis on D11 and D121 , we obtain a
derivation:
D0121 :: (Γ1 , Γ1 , Γ2 , [A]R1 ∩R2 )

Lemma 2.6 (n-cut). Assume that R1 , R2 , . . . , Rn are subsets of R
for some n ≥ 1 such that:

By applying the rule (!-neg-contract) to D0121 repeatedly,
we obtain a derivation of (Γ1 , Γ2 , [A]R1 ∩R2 ).
D2 is of the following form:

Then the following rule is admissible in LMRL∧ :

D21 :: Γ2 , {[A]R2 }, [A]R2
` Γ2 , {[A]R2 }

R1 ] R2 ] . . . ] Rn = ∅
(Γ1 , [A]R1 ; Γ2 , [A]R2 ; . . . ; Γn , [A]Rn ) ⇒ Γ1 , Γ2 , . . . , Γn

(!-neg-contract)

Proof. Assume Di :: (Γ1 , [A]Ri ) for 1 ≤ i ≤ n. The proof proceeds
by induction on n. The base case (where n = 1) is simply covered
by Lemma 2.2. For n ≥ 2, we can apply Lemma 2.4 to D1 and
D2 to obtain a derivation D12 :: (Γ1 , Γ2 , [A]R12 ) where R12 =
R1 ∩ R2 . Clearly, R12 = R1 ] R2 holds, and we can invoke induction
hypothesis on D12 and the remaining derivations Di for 3 ≤ i ≤ n
to obtain a derivation of (Γ1 , . . . , Γn ).


We simply obtain a derivation of (Γ1 , Γ2 , [A]R1 ∩R2 ) by the
induction hypothesis on D1 and D21 .
• Assume r < R1 and r ∈ R2 . This subcase is completely analogous to the previous one.
• Assume r ∈ R1 and r ∈ R2 . Then Dk is of the following form
for each of the cases k = 1 and k = 2:
Dk1 :: ?(Γk ), [B]Rk
(!-pos)
` ?(Γk ), [A]Rk

Lemma 2.7 (Splitting). The following rule is admissible in LMRL∧ :
(Γ, [A]R1 ]R2 ) ⇒ Γ, [A]R1 , [A]R2

D012

We obtain
:: (?(Γ1 ), ?(Γ2 ), [B]R1 ∩R2 ) by the induction hypothesis on D11 and D21 . We then obtain a derivation of
(?(Γ1 ), ?(Γ2 ), [A]R1 ∩R2 ) by applying the rule (!-pos) to D012 .

Proof. Assume D1 :: (Γ, [A]R1 ]R2 ). By Lemma 2.3, we have a
derivation:
D2 :: ([A]R1 ∩R2 , [A]R1 , [A]R2 )

Assume A is of the form ∀r (λx.B). We have three possibilities:
r ∈ R1 and r < R2 , or r ∈ R2 and r < R1 , or r ∈ R1 and r ∈ R2 .

By applying Lemma 2.5 to D1 and D2 , we obtain a derivation of
(Γ, [A]R1 , [A]R2 ).


• Assume r ∈ R1 and r < R2 . Then D1 is of the following form:

D11 :: (Γ1 , [B]R1 )
` Γ, [A]R1

2.3

(∀-pos)

where x does not have any free occurrences in Γ1 , and D2 is of
the following form:
D21 :: (Γ2 , [B{x/t}]R2 )
` Γ, [A]R2

LMRL∨ as the Dual of LMRL∧ : Disjunctive LMRL

For a bit of completeness, we introduce disjunctive LMRL (LMRL∨ ),
which is the exact dual of LMRL∧ . The inference rules for LMRL∨
are listed in Figure 3, which can simply be obtained by replacing
each set (of roles) in Figure 2 with its complement. The various
lemmas established for LMRL∧ are given their counterparts in
LMRL∨ as follows:

(∀-neg)

Let D011 be D11 {x/t}, which is a derivation of (Γ1 , [B{x/t}]R1 ).
By the induction hypothesis on D011 and D21 , we have a derivation:
D121 :: (Γ1 , Γ2 , [B{x/t}]R1 ∩R2 )

Lemma 2.8. The following rule is admissible in LMRL∨ :
(Γ, [A]∅ ) ⇒ Γ
Note that Lemma 2.8 simply states the admissibility of the cutrule n-cut-disj for n = 1.

By applying the rule (∀-neg) to D121 , we have a derivation of
(Γ1 , Γ2 , [A]R1 ∩R2 ).
• Assume r < R1 and r ∈ R2 . Then this case is analogous to the
previous one.
• Assume r ∈ R1 and r ∈ R2 . Then Dk is of the following form
for each of the cases k = 1 and k = 2:
Dk1 :: (Γk , [A]Rk , [B]Rk )
(∀-pos)
` Γk , [A]Rk

Lemma 2.9 (η-expansion). The following rule is admissible in
LMRL∨ :
() ⇒ [A]R1 , . . . , [A]Rn
where R1 ] . . . ] Rn = ∅.
Lemma 2.10 (2-cut). The following rule is admissible in LMRL∨ :
(Γ1 , [A]R ; Γ2 , [A]R ) ⇒ Γ1 , Γ2

where x does not have free occurrences in Γk . By the induction
hypothesis on D11 and D21 , we have a derivation:

Lemma 2.11 (2-cut with spill). Assume that R1 and R2 are disjoint.
Then the following rule is admissible in LMRL∨ :

D012 :: (Γ1 , Γ2 , [B]R1 ∩R2 )

(Γ1 , [A]R1 ; Γ2 , [A]R2 ) ⇒ Γ1 , Γ2 , [A]R1 ]R2

By applying the rule (∀-pos) to D012 , we obtain a derivation of
(Γ1 , Γ2 , [A]R1 ∩R2 ).

Lemma 2.12 (Multi-cut). Assume that R1 , R2 , . . . , Rn are subsets
of R for some n ≥ 2 such that:
R1 ] R2 ] . . . ] Rn = ∅

All of the cases are covered where the cut-formula is the major
formula of both D1 and D2 . For brevity, we omit the cases where
the cut-formula is not the major formula of either D1 or D2 , which
can be trivially handled (Troelstra 1992).


Then the following rule is admissible in LMRL∨ :
(Γ1 , [A]R1 ; Γ2 , [A]R2 ; . . . ; Γn , [A]Rn ) ⇒ Γ1 , Γ2 , . . . , Γn

6

2018/3/1

R1 ] . . . ] Rn = ∅
(Id∨ )
` [a]R1 , . . . , [a]Rn

P

r ∈ R ` Γ, [A]R , [B]R
(O-pos)
` Γ, [A ⊗r B)]R
r<R

` Γ1 , [A]R ` Γ2 , [B]R
(O-neg)
` Γ1 , Γ2 , [A ⊗r B]R
r ∈ R ` Γ, [A]R
(⊕-pos-l)
` Γ, [A &r B]R
r ∈ R ` Γ, [B]R
(⊕-pos-r)
` Γ, [A &r B]R

r<R

` Γ, [A]R ` Γ, [B]R
(⊕-neg)
` Γ, [A &r B]R

linking
name input (r < R)
name output (r ∈ R)
empty input (r < R)
empty output (r ∈ R)
case offer (r < R)
left choice (r ∈ R)
right choice (r ∈ R)
server accept (r < R)
client request (r ∈ R)

Note that 1 is the unit of ⊗ in CLL. It is also clear that the presence
of the rule (not∧ ) invalidates the admissibility of n-cut for any
n , 2. Let us take a look at the case where n = 3. Applying a
3-cut to (Γ, [¬A]R1 ), (Γ, [¬A]R2 ), and (Γ, [¬A]R3 ) requires that the
condition R1 ] R2 ] R3 = ∅ be met; this 3-cut is supposed to be
reduced to another 3-cut on (Γ, [A]R1 ), (Γ, [A]R2 ), and (Γ, [A]R3 );
this new 3-cut is unfortunately not valid since it requires that the
condition R1 ] R2 ] R3 = ∅ be met (which contradicts the previous
condition R1 ] R2 ] R3 = ∅).
We see LMRL as a form of negation-less logic: The negation
of each i-formula [A]R is simply the i-formula [A]R but there is
no negation for the formula A per se. In other words, the notion
of negation cannot be internalized within LMRL if 3-cut is to be
preserved.

r∈R `Γ
(?-pos-weaken)
` Γ, [!r (A)]R
r ∈ R ` Γ, [A]R
(?-pos-derelict)
` Γ, [!r (A)]R
` Γ, [!r (A)]R , [!r (A)]R
(?-pos-contract)
` Γ, [!r (A)]R

r ∈ R ` Γ, [A{t/x}]R
(∃-pos)
` Γ, [∀r (λx.A)]R

3.

r < R x < Γ ` Γ, [A]R
(∃-neg)
` Γ, [∀r (λx.A)]R

LMRL as a Process Calculus

As the inspiration for LMRL stems from studies on multiparty session types, it only seems fit if we present a typed variant (πLMRL)
of π-calculus (Milner et al. 1992c) in which the types are directly
based on the formulas in LMRL. We are to closely follow some recent work by Caires and Pfenning (2010) and Wadler (2012) in our
presentation of πLMRL. In particular, we shall mostly adopt the
notational convention used by the latter and thus refer the reader to
the original paper for detailed explanation.
We see the encoding of cut-elimination of LMRL in πLMRL
mostly as a routine exercise. However, it should be noted that there
exists a fundamental difference between πLMRL and π-calculus:
The point-to-point communication in the latter is replaced with
a form of broadcasting in the former. We are to mention at the
end a simple extension of πLMRL that can support point-to-point
communication directly.

Figure 3. The inference rules for LMRL∨
Lemma 2.13 (Co-Splitting). The following rule is admissible in
LMRL∨ :
(Γ, [A]R1 ∩R2 ) ⇒ Γ, [A]R1 , [A]R2
where R1 and R2 are disjoint.
The proofs for these lemmas (2.8, 2.10, 2.11, 2.12, and 2.13)
are omitted as they are completely analogous to those for the
corresponding lemmas in LMRL∧ .
2.4

~
νx : A.(P)
xR (y)r .(P1 | P2 )
xR [y]r .P
xR ( )r .0
xR [ ]r .P
xR (case)r .(P1 , P2 )
xR [inl]r .P
xR [inr]r .P
!xR (y)r
?xR [y]r

Figure 4. The syntax for processes in πLMRL

r < R ` ?(Γ), [A]R
(?-neg)
` ?(Γ), [!r (A)]R

r∈R

::=

About LMRL and Negation

3.1

Given an i-formula [A]R , we may think of the i-formula [A]R as the
negation of [A]R . For the moment, let us use ¬A for the negation of
A and introduce the following rule for handling negation:
Γ, [A]R
(not∧ )
Γ, [¬A]R

Session Types

The session types (or types for short) are just formulas in LMRL
except for adding 1r (the unit for ⊗r ) for each role r and dropping
primitive formulas as well as quantified formulas:
Session Types

It is clear that LMRL∧ extended with the rule (not∧ ) corresponds
precisely to CLL if the underlying set ∅ of roles equals {0, 1}. The
logical connective ∧0 and ∧1 correspond to ∧ and ∨, respectively,
and the quantifiers ∀0 and ∀1 correspond to ∀ and ∃, respectively.
Each sequent Γ in LMRL∧ can be translated into a sequent A1 ` A0
as follows such that Γ is derivable in LMRL∧ if and only if A1 ` A0
is derivable in CLL:

A

::=

1r | A1 ⊗r A2 | A1 &r A2 | !r (A)

The meaning of various forms of session types is to be given later.
3.2

Process Terms

The syntax for the terms representing processes in πLMRL are
given in Figure 3.1. We use x and y for names (of channels). Given
x and R, the term xR refers to an endpoint of the name x such that
the endpoint is supposed to be held by a party playing the roles
~ for a sequence of
contained in R. We use P for a process and P
~ the name x is
the form (P1 | . . . | Pn ) where n ≥ 1. In νx : A.(P),
~
bound in P; in xR (y)r .(P1 | P2 ), the name y is bound in P1 (but
not in P2 ); in xR [y]r , !xR (y)r , and ?xR [y]r , the name y is bound in
P. Given a process P, we write fn(P) for the set of free names

• If [A]∅ is in Γ, then 1 goes into A0 ;
• If [A]∅ is in Γ, then 1 goes into A1 ;
• If [A]{0} is in Γ, then A goes into A0 ;
• If [A]{1} is in Γ, then A goes into A1 .

7

2018/3/1

in P. Note that the presence of annotations like A, R, and r in
process terms is solely for supporting a form of Church typing.
Such annotations may be omitted if there is no risk of confusion.
In particular, they are not needed in the formulation of reduction
semantics for πLMRL.
Given P1 , . . . , Pn for some n ≥ 2, νx.(P1 | . . . | Pn ), which is
often referred to as a cut, means to link n endpoints xRi for some
name x and role sets R1 , . . . , Rn such that R1 ] . . . ] Rn = ∅ and each
xRi is contained in Pi for 1 ≤ i ≤ n.
The meaning of various headers in Figure 3.1 is to be made
clear when the reduction semantcs for πLMRL is formulated. For
the moment, we present a bit of intuition on them as follows.
A header term xR (y)r means that r ∈ R holds and an name
is to be received on the endpoint xR . Normally, substitution of
the received name for y would take place explicitly. As y is a
bound variable, another option, which we take here, is to rename y
implicitly to match the received name. Dually, a header term xR [y]r
means that r < R holds and a fresh name is to be chosen and then
sent onto the endpoint xR .
A header term xR [ ]r means a send action is to take place on xR
but no name is actually sent. Dually, a header term xR ( )r means
a recieve action is to take place on xR but no name is actually
received.
A header term xR [inl]r (xR [inr]r ) means that a left (right) choice
is to be sent onto the endpoint xR . A header term xR (case)r means
that either a left or right choice is to be received on the endpoint
xR and the received choice determines which of the two processes
following the header should be chosen.
A header term !xR [y]r essentially means that it can be repeatly
used as xR [y]r , and a header term ?xR (y)r is like xR (y)r but it is
supposed to match !xR [y]r .
3.3

R1 ] . . . ] Rn = ∅

Pi ` Γi , x : [A]Ri for 1 ≤ i ≤ n

νx.(P1 | . . . | Pn ) ` Γ1 , . . . , Γn

(n-cut)

r < R P ` Γ, y : [A1 ]R , x : [A2 ]R
(⊗-neg)
x[y]r .P ` Γ, x : [A1 ⊗r A2 ]R
r ∈ R P1 ` Γ1 , y : [A1 ]R P2 ` Γ2 , x : [A2 ]R
(⊗-pos)
x(y)r .(P1 , P2 ) ` Γ1 , Γ2 , x : [A1 ⊗r A2 ]R
r∈R P`Γ
(1-neg)
xR [ ]r .P ` Γ, x : [1r ]R

r∈R
(1-pos)
xR ( )r .0 ` x : [1r ]R

r < R P ` Γ, x : [A1 ]R
(&-neg-l)
xR [inl]r .P ` Γ, x : [A1 &r A2 ]R
r < R P ` Γ, x : [A2 ]R
(&-neg-r)
xR [inr]r .P ` Γ, x : [A1 &r A2 ]R
r ∈ R P1 ` Γ, x : [A1 ]R P2 ` Γ, x : [A2 ]R
(&-pos)
xR (case)r .(P1 , P2 ) ` Γ, x : [A1 &r A2 ]R
r ∈ R P ` Γ, y : [A]R
(!-pos)
!xR (y)r .P ` Γ, x : !r (A)
r∈R P`Γ
(!-neg-weaken)
P ` Γ, x : !r (A)
r ∈ R P ` Γ, y : [A]R
(!-neg-derelict)
?xR [y]r .P ` Γ, x : !r (A)
r∈R

Statics of πLMRL

P ` Γ, x0 : [!r (A)]R , x : [!r (A)]R
(!-neg-contract)
P{x/x0 } ` Γ, x : !r (A)
Figure 5. The typing rules for πLMRL

Given a type and a role set R, we can form an i-type [A]R . If one
thinks that A is a global type, then [A]R is a local type for the
endpoint of a full channel that is supposed to be held by a party
playing the roles in R. The meaning for various forms of session
types is to become clear when the typing rules in πLMRL are
presented.
Let us write [A ⊗ B]R ([AOB]R ) to mean [A ⊗r B]R for some
r ∈ R (r < R). In the literature, A ⊗ B is often intuitively interpreted
as output A then behave as B (Caires and Pfenning 2010; Wadler
2012a), but we are to see that it cannot be the case in πLMRL; it
must be interpreted as input A then behave as B as is stipulated by
the proof of cut-elimination. Dually, AOB must be interpreted as
output A then behave as B in πLMRL. Let us write [A&B]R ([A ⊕
B]R ) to mean [A&r B]R for some r ∈ R (r < R); A&B intuitively
means offering choice of A or B and A ⊕ B means selecting from
A or B. Let us write [!A]R ([?A]R ) to mean [!r A]R for some r ∈ A
(r < A); !A means the ability to repeatedly spawn processes of the
type A while ?A means to request such a process to be spawned.
In πLMRL, we use Γ for an environment associating distinct
names with i-types. Let Γ be the following environment:

3.4

Dynamics of πLMRL

We present a reduction semantics for πLMRL based on Lemma 2.6,
which states the admissibility of the following rule in LMRL:
(Γ1 , [A]R1 ; Γ2 , [A]R2 ; . . . ; Γn , [A]Rn ) ⇒ Γ1 , Γ2 , . . . , Γn
where R1 ] R2 ] . . . ] Rn = ∅ is assumed. Ideally, we would
formulate such a reduction semantics by directly following the
proof of Lemma 2.6, which essentially implies following the proof
of Lemma2.4. Unfortuately, it is not yet clear to us how the latter
can be encoded in a process calculus. Instead, we are to proceed by
following a direct proof of Lemma 2.6, which is largely parallel to
a standard proof of cut-elimination for classical linear logic (e.g.,
the one used by Wadler (2012)).
We use ≡ for a structural equivalence relation on processes and
assume it to contain the following equivalence rules (perm) and
(assoc):

x1 : [A1 ]R1 , . . . , xn : [An ]Rn

(perm)
(assoc)

Then the domain dom(Γ) of Γ equals {x1 , . . . , xn }. Given another
environment Γ0 , we write Γ, Γ0 for the union of Γ and Γ1 whenever
dom(Γ) ∩ dom(Γ0 ) = ∅. We refer to x : [A]R as an association in an
environment.
A typing judgment in πLMRL is of the form

~ 1 ) ≡ νx.(P
~2)
νx.(P
~1) | P
~ 2 ) ≡ νy.(νx.(P | P
~2) | P
~1)
νx.(νy.(P | P

~ 2 is assumed to be a permutation of P
~ 1 . For (assoc),
For (perm), P
both x ∈ fn(P1 ) and y ∈ fn(P1 ) are assumed to hold.
Let us assume a typing derivation D of the following form
(where the last applied rule is (n-cut) for n ≥ 2):

P ` x1 : [A1 ]R1 , . . . , xn : [An ]Rn

R1 ] . . . ] Rn = ∅

meaning that process P communicates along each endpoint (xi )Ri
in a full channel specified by the session type Ak for k = 1, . . . , n.
Erasing P and the names xk from the judgment yields a judgment
in LMRL (extended with 1r (as the unit for ⊗r ) for each role r).

Di :: Pi ` Γi , x : [A]Ri for 1 ≤ i ≤ n

νx.(P1 | P2 | . . . | Pn ) ` Γ1 , Γ2 , . . . , Γn
The cut νx.(P1 | P2 | . . . | Pn ) is a principal cut if each association
x : [A]Ri is introduced by the last applied rule in Di .
8

2018/3/1

We use ⇒ for a single-step reduction relation on processes. We
first introduce proper rules for reducing principal cuts and then
introduce another set of rules for handling non-principal cuts (based
on so-called commuting conversions).

~ ⇒ x[y].νx0 .(P1 | P)
~
νx0 .(x[y].P1 | P)
~ ⇒ x(y).(νx0 .(P1 | P)
~ | P2 )
νx0 .(x(y).(P1 | P2 ) | P)
if x0 ∈ fn(P1 )
~ ⇒ x(y).(P1 | νx0 .(P2 | P))
~
νx0 .(x(y).(P1 | P2 ) | P)
if x0 ∈ fn(P2 )
~ ⇒ x[inl].νx0 .(P1 | P)
~
νx0 .(x[inl].P1 | P)
~
~
νx0 .(x[inr].P1 | P) ⇒ x[inr].νx0 .(P1 | P)
~
~ P2 | P)
~
νx0 .(x(case).(P1 , P2 ) | P) ⇒ x(case).νx0 .(P1 | P,
~
~
νx0 .(!x[y].P1 | P) ⇒ !x[y].νx0 .(P1 | P)
~ ⇒ ?x[y].νx0 .(P1 | P)
~
νx0 .(?x[y].P1 | P)

Rules for principal cuts Let assume that νx.(P1 | P2 | . . . | Pn ) is
principal cut for the moment. Based on the outmost type constructor in A, we have four cases of elimination of principal cuts:
• Assume that A is of the form A1 ⊗r A2 . Without loss of generality,

we may assume r ∈ R1 , that is, r < R1 . Then r < Ri for 2 ≤ i ≤ n,
implying r ∈ Ri for 2 ≤ i ≤ n. It is clear that P1 is of the
form xR1 [y]r .(P01 ) and Pi of the form xRi (y)r .(P0i | P1i ) for each
2 ≤ i ≤ n. Therefore νx.(P1 | P2 | . . . | Pn ) can be reduced to the
following process Q1 :

Figure 6. The rules for commuting conversions
r ∈ R ∧ s ∈ R P ` Γ, x : [A]R
(msg-pos-pos)
xR (skip)r,s .P ` Γ, x : [msgr,s (A)]R

νx.(νy.(P01 | P02 | . . . | P0n ) | P12 | . . . | P1n )
which performs a cut of A1 followed by a cut of A2 . It can also
be reduced to the following process Q2 :

r < R ∧ s < R P ` Γ, x : [A]R
(msg-neg-neg)
xR [skip]r,s .P ` Γ, x : [msgr,s (A)]R

νy.(νx.(P01 | P12 | . . . | P1n ) | P02 | . . . | P0n )

r ∈ R ∧ s < R P ` Γ, x : [A]R
(msg-pos-neg)
xR (recv)r,s .P ` Γ, x : [msgr,s (A)]R

which performs a cut of A2 followed by a cut of A1 . Note that
Q1 and Q2 are structurally equivalent, that is Q1 ≡ Q2 holds.
There is a bit of surprise here as [A1 ⊗ A2 ]R (which is [A1 ⊗r A2 ]R
for r ∈ R) is interpreted as input A1 and then behave as A2 .
If it is interpreted as output A1 and then behave as A2 (which
is commonly done in studies on dyadic session types (e.g.,
(Caires and Pfenning 2010; Wadler 2012a))), then each process
Pi needs to send a message to P1 for 2 ≤ i ≤ n, performing a
kind of reverse broadcasting.

r < R ∧ s ∈ R P ` Γ, x : [A]R
(msg-neg-pos)
xR [send]r,s .P ` Γ, x : [msgr,s (A)]R
Figure 7. Typing rules for msgr,s
We have covered all of the possible cases for P1 .

• Assume that A is of the form 1r . Without loss of generality, we

may assume r < A1 and r ∈ Ai for 2 ≤ i ≤ n. Clearly, P1 is of the
form xR1 [ ]r .P01 and Pi of the form xRi ( )r .0 for each 2 ≤ i ≤ n.
Then we have

Please find in Figure 8 some detailed illustration of the reduction
rules for eliminating principal cuts.
Rules for non-principal cuts The rules for handling non-principal
cuts are based on commuting conversions, each of which pushes
a cut inside a communication header. If can be readily checked
that a cut must be a principal one of none of the rules in Figure 6
are applicable. Please see (Wadler 2014) for details on commuting
conversions.

νx.(P1 | P2 | . . . | Pn ) ⇒ P01
Note that the last applied rule in D1 is (1-neg). and the last
applied rule in Di is (1-pos) for 2 ≤ i ≤ n.
• Assume that A is of the form A1 ⊕r A2 . Without loss of generality,

we may assume r < A1 and r ∈ Ai for 2 ≤ i ≤ n. It is clear that
P1 is of the form xR1 [inl]r .(P01 ) or xR1 [inr]r .(P11 ), and Pi is of the
form xRi (case)r .(P0i | P1i ). Therefore νx.(P1 | P2 | . . . | Pn ) can be
reduced to the following process

3.5

Subject Reduction and Cut-Elimination

Let us define P =⇒ Q as P ≡ P1 and P1 ⇒ Q1 and Q1 ≡ Q for
some P1 and Q1 . Let =⇒∗ be the transitive closure of =⇒.
Theorem 3.1 (Subject Reduction). Assume that P ` Γ is derivable.
If P =⇒ P0 , then P0 ` Γ is also derivable.

νx.(Pk1 | Pk2 | . . . | Pkn )
where k = 0 or k = 1 (depending on whether inl or inr occurs
in the header of P1 ).

Proof. It simply follows the way in which =⇒ is defined.

• Assume that A is of the form !r (B). Without loss of generality,



Theorem 3.2 (Cut-Elimination). Assume that P ` Γ is derivable.
If P is a cut, then P =⇒ P0 holds for some P0 .

we may assume r < A1 and r ∈ Ai for 2 ≤ i ≤ n. It is clear that
each Pi is of the form !xRi (y)r .(P0i ) for 2 ≤ i ≤ n. As for P1 ,
there are three possibilities.

Proof. (Sketch) It follows from a simple case analysis on P. For
details, one may see the proof of Theorem 2 (Wadler 2014). Note
that we use cut-elimination in a rather liberal sense: It means the
elimination of a particular cut (and P0 may be allowed to contain
cuts). The point is to guarante progress being made (rather than the
eventuality of reaching some sort of terminal state).


The name x is not in fn(P1 ). Then we have
νx.(P1 | P2 | . . . | Pn ) ⇒ P1
P1 is of the form ?xR1 [y]r .P01 for some P01 and x < fn(P01 ).
Then we can have
νx.(P1 | P2 | . . . | Pn ) ⇒ νy.(P01 | P02 | . . . | P0n )

3.6

Support for Point-to-Point Communication

By inspecting the reduction rules in πLMRL that involve communication, we can clearly see that only communication in the form of
broadcasting is involved. However, it is rather simple to support
point-to-point communication by extending πLMRL with unary
type constructors msgr,s , where r and s range over all of the distinct pairs of roles.

P1 is of the form P01 {x/x0 } for some P01 and x ∈ fn(P01 ). Then
we can have
νx.(P1 | P2 | . . . | Pn ) ⇒
νx.(νx0 .(P1 | P02 | . . . | P0n ) | P2 | . . . | Pn )
where P0i = !x0 Ri (y)r .(P0i ) for 2 ≤ i ≤ n.
9

2018/3/1

G. Bellin and P. J. Scott. On the pi-Calculus and Linear Logic. Theor.
Comput. Sci., 1994a.
G. Bellin and P. J. Scott. On the pi-calculus and linear logic. Theor. Comput.
Sci., 135(1):11–65, 1994b. doi: 10.1016/0304-3975(94)00104-9. URL
http://dx.doi.org/10.1016/0304-3975(94)00104-9.
L. Caires and J. A. Pérez. Multiparty session types within a canonical binary
theory, and beyond. International Conference on Formal Techniques for
. . . , 2016.
L. Caires and F. Pfenning. Session types as intuitionistic linear propositions.
In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, pages 222–236, 2010. doi: 10.1007/978-3-642-15375-4\ 16.
URL http://dx.doi.org/10.1007/978-3-642-15375-4_16.
M. Carbone, F. Montesi, C. Schürmann, and N. Yoshida. Multiparty Session
Types as Coherence Proofs. CONCUR, pages 412–426, 2015.
M. Carbone, S. Lindley, F. Montesi, and C. Schürmann. Coherence Generalises Duality: a logical explanation of multiparty session types. In
CONCUR, pages 33:1–33:14, 2016.
G. Castagna, M. Dezani-Ciancaglini, E. Giachino, and L. Padovani. Foundations of session types. In Proceedings of the 11th International ACM
SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pages 219–230,
2009. doi: 10.1145/1599410.1599437. URL http://doi.acm.org/
10.1145/1599410.1599437.
S. J. Gay and V. T. Vasconcelos. Linear type theory for asynchronous
session types. J. Funct. Program., 20(1):19–50, 2010. doi: 10.
1017/S0956796809990268. URL http://dx.doi.org/10.1017/
S0956796809990268.
G. Gentzen. Untersuchungen über das logische Schlieβen. Mathematische
Zeitschrift, 39:176–210, 405–431, 1935.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–101,
1987.
K. Honda.
Types for dyadic interaction.
In CONCUR ’93, 4th
International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, pages 509–523, 1993. doi:
10.1007/3-540-57208-2\ 35. URL http://dx.doi.org/10.1007/
3-540-57208-2_35.
K. Honda, V. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In Programming Languages and Systems - ESOP’98, 7th European Symposium on
Programming, Held as Part of the European Joint Conferences on the
Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March
28 - April 4, 1998, Proceedings, pages 122–138, 1998. doi: 10.1007/
BFb0053567. URL http://dx.doi.org/10.1007/BFb0053567.
K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273–284, 2008. doi:
10.1145/1328438.1328472. URL http://doi.acm.org/10.1145/
1328438.1328472.
S. Lindley and J. G. Morris. A semantics for propositions as sessions.
In Programming Languages and Systems - 24th European Symposium
on Programming, ESOP 2015, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2015, London,
UK, April 11-18, 2015. Proceedings, pages 560–584, 2015. doi: 10.
1007/978-3-662-46669-8\ 23. URL http://dx.doi.org/10.1007/
978-3-662-46669-8_23.
R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes, I. Inf.
Comput., 1992a.
R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes, II.
Inf. Comput., 1992b.
R. Milner, J. Parrow, and D. Walker. A calculus of processes, parts I and II.
Information and Computation, 100:1–40 and 41–77, 1992c.
R. Neykova and N. Yoshida. Multiparty Session Actors. COORDINATION,
pages 131–146, 2014.
J. A. Pérez, L. Caires, F. Pfenning, and B. Toninho. Linear Logical Relations for Session-Based Concurrency. In Programming Languages

νx.(x[skip].P1 | x(skip).P2 | . . . | x(skip).Pn )
⇒ νx.(P1 | P2 | . . . | Pn )
νx.(x[send].P1 | x(recv).P2 | x(skip).P3 | . . . | x(skip).Pn )
⇒ νx.(P1 | P2 | P3 | . . . | Pn )

4.

Related Work and Conclusion

Session types were introduced by Honda (Honda 1993) and further
extended subsequently (Takeuchi et al. 1994; Honda et al. 1998).
There have since been extensive theoretical studies on session types
in the literature(e.g., (Castagna et al. 2009; Gay and Vasconcelos
2010; Caires and Pfenning 2010; Toninho et al. 2011b; Vasconcelos 2012; Wadler 2012a; Lindley and Morris 2015)). Multiparty
session types, as a generalization of (dyadic) session types, were
introduced by Honda and others (Honda et al. 2008), together with
the notion of global types, local types, projection and coherence.
Introduced by Milner and others (Milner et al. 1992a,b), πcalculus allows channel names to be communicated along the channels themselves, making it possible to describe concurrent computations with changing network configuration. Connections between
π-calculus and linear logic have been actively studied (Abramsky
1994b; Bellin and Scott 1994a) from early on, and it is demonstrated in some recent work (Caires and Pfenning 2010; Wadler
2012b, 2014) that a tight proofs-as-processes correspondences exists for dyadic sessions. And some of closely related additional
work includes Toninho et al. (2011a); Pfenning et al. (2011); Toninho et al. (2012); Pérez et al. (2012).
Continuing this line of works, Carbone (Carbone et al. 2015)
introduced MCP, a variant of CLL that admits MCut, a generalized
cut-rule for composing multiple proofs. MCut requires coherent
proofs (obtained through a separate proof system) as a side condition. This work is probably the first along the line that interprets
 as input and O as output (as opposed to all of the other works
we are aware of). Their follow-up work (Carbone et al. 2016) introduced a variant of MCP, and a translation from MCP to CP (Wadler
2012b) via GCP (some intermediate calculus) that interprets a coherence proof as an arbiter process that mediates communications
in a multiparty session. But it reverts to  as output and O as input.
In this paper, we take a very different route to formulate a cut-rule
for multiple sequents, naturally extending the celebrated result of
cut-elimination by Gentzen.
There have been studies on multirole parties (Yoshida and
Deniélou 2011; Neykova and Yoshida 2014), where such parties
play multiple roles by holding channels belonging to multiple sessions. We see no direct relation between a multirole party and a
multirole channel as is formulated in this paper.
There is also very recent work on encoding multiparty session
types based on binary session types (Caires and Pérez 2016), which
relies on an arbiter process to mediate communications between
multiple parties while preserving global sequencing information.
Clearly, this form of mediating (formulated based on automata
theory) is closely related to performing a cut to multiple processes
in πLMRL.
While multirole logic stems from studies on multiparty session
types, it is certainly not restricted to such studies. Just as the notion
of linearity (as in linear logic) that has greatly enriched the study
on logics and programming languages, we hope that the notion of
multirole (as in multirole logic) can exert a significant impact in
this regard as well.

References
S. Abramsky. Proofs as processes. Theor. Comput. Sci., 135(1):5–9, 1994a.
doi: 10.1016/0304-3975(94)00103-0. URL http://dx.doi.org/10.
1016/0304-3975(94)00103-0.
S. Abramsky. Proofs as Processes. Theor. Comput. Sci., 1994b.

10

2018/3/1

id(x1 , x) ` x1 , x

Axiom

Axiom
Axiom
id(x2 , x) ` x2 , x
id(x3 , x) ` x3 , x
3-Cut
νx.(id(x1 , x) | id(x2 , x) | id(x3 , x)) ` x1 , x2 , x3
=⇒

id(x1 , x2 , x3 ) ` x1 , x2 , x3

Axiom

(βAx )

r ∈ R3 P3 ` y3 Q3 ` x
r ∈ R2 P2 ` y2 Q2 ` x
r < R1 P ` y, x
-pos
-pos
-neg
x[y].P ` x
x(y2 ).(P2 |Q2 ) ` x
x(y3 ).(P3 |Q3 ) ` x
3-Cut
νx.(x[y].P | x(y2 ).(P2 | Q2 ) | x(y3 ).(P3 | Q3 )) ` ·
P ` y, x Q2 ` x Q3 ` x
3-Cut
νx.(P | Q2 | Q3 ) ` y
P2 {y/y2 } ` y P3 {y/y3 } ` y
=⇒
3-Cut
νy.(νx.(P | Q2 | Q3 ) | P2 {y/y2 } | P3 {y/y3 }) ` ·

(β )

r ∈ R3 P3 ` x Q3 ` x
r < R1 P ` x
r ∈ R2 P2 ` x Q 2 ` x
N-neg-l
N-pos
N-pos
x[inl].P ` x
x.case(P2 , Q2 ) ` x
x.case(P3 , Q3 ) ` x
3-Cut
νx.(x[inl].P | x.case(P2 , Q2 ) | x.case(P3 , Q3 )) ` ·
P ` x P2 ` x P3 ` x
3-Cut
νx.(P|P2 |P3 ) ` ·

(βNl )

=⇒

P ` x Q2 ` x Q3 ` x
3-Cut
νx.(P|Q2 |Q3 ) ` ·

(βNr )

=⇒

P`·

=⇒
r ∈ R3 P3 ` x Q3 ` x
r ∈ R2 P2 ` x Q 2 ` x
r < R1 P ` x
N-neg-r
N-pos
N-pos
x[inr].P ` x
x.case(P2 , Q2 ) ` x
x.case(P3 , Q3 ) ` x
3-Cut
νx.(x[inr].P | x.case(P2 , Q2 ) | x.case(P3 , Q3 )) ` ·

r ∈ R2
r < R1 P ` ·
1-pos
1-neg
0`x
P`x
νx.(P | 0 | 0) ` ·

r ∈ R3
1-pos
0`x

3-Cut

(β1 )

r ∈ R3 P3 ` y3
r ∈ R2 P2 ` y2
r < R1 P ` y
!-neg-derelict
!-pos
!-pos
?x(y).P ` x
!x(y2 ).P2 ` x
!x(y3 ).P3 ` x
3-Cut
νx.(?x[y].P | !x(y2 ).P2 | !x(y3 ).P3 ) ` ·
=⇒
r ∈ R3 P3 ` y3
r < R1 P ` ·
r ∈ R2 P2 ` y2
!-neg-weaken
!-pos
!-pos
P`x
!x(y2 ).P2 ` x
!x(y3 ).P3 ` x
3-Cut
νx.(P | !x(y2 ).P2 | !x(y3 ).P3 ) ` ·

P ` y P2 {y/y2 } ` y P3 {y/y3 } ` y
3-Cut
νy.(P | P2 {y/y2 } | P3 {y/y3 }) ` ·

(β! )

P`·
!-neg-weaken
P`·

(β!W )

r ∈ R3 P03 ` y3
r ∈ R2 P02 ` y2
!-pos
!-pos
0
!m(y2 ).P2 ` m
!m(y3 ).P03 ` m
r ∈ R3 P003 ` y3
r ∈ R2 P002 ` y2
3-Cut
!-pos
!-pos
0
0
νm.(P | !m(y2 ).P2 | !m(y3 ).P3 ) ` n
!n(y2 ).P002 ` n
!n(y3 ).P003 ` n
3-Cut
0
0
00
00
νn.(νm.(P | !m(y2 ).P2 | !m(y3 ).P3 ) | !n(y2 ).P2 | !n(y3 ).P3 ) ` ·
!-neg-contract
νn.(νm.(P | !m(y2 ).P2 | !m(y3 ).P3 ) | !n(y2 ).P2 | !n(y3 ).P3 ) ` ·

(β!C )

=⇒

r < R1 P ` m, n
r ∈ R3 P3 ` y3
r ∈ R2 P2 ` y2
!-neg-contract
!-pos
!-pos
P{x/m, n} ` x
!x(y2 ).P2 ` x
!x(y3 ).P3 ` x
3-Cut
νx.(P{x/m, n} | !x(y2 ).P2 | !x(y3 ).P3 ) ` ·
P ` m, n
=⇒

Figure 8. Principal Cut Reduction for 3-Party Sessions
Without loss of generality, we present here a 3-party principal cut reduction without proof terms. Assume R1 ] R2 ] R3 = ∅ and r < R1

11

2018/3/1

and Systems, pages 539–558. Springer Berlin Heidelberg, Berlin, Heidelberg, Mar. 2012.
F. Pfenning, L. Caires, and B. Toninho. Proof-Carrying Code in a SessionTyped Process Calculus. CPP, 7086(Chapter 4):21–36, 2011.
K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and
its typing system. In PARLE ’94: Parallel Architectures and Languages
Europe, 6th International PARLE Conference, Athens, Greece, July 4-8,
1994, Proceedings, pages 398–413, 1994. doi: 10.1007/3-540-58184-7\
118. URL http://dx.doi.org/10.1007/3-540-58184-7_118.
B. Toninho, L. Caires, and F. Pfenning. Dependent session types via
intuitionistic linear type theory. In Proceedings of the 13th international
. . . , 2011a.
B. Toninho, L. Caires, and F. Pfenning. Dependent session types via
intuitionistic linear type theory. In Proceedings of the 13th International
ACM SIGPLAN Conference on Principles and Practice of Declarative
Programming, July 20-22, 2011, Odense, Denmark, pages 161–172,
2011b. doi: 10.1145/2003476.2003499. URL http://doi.acm.org/
10.1145/2003476.2003499.
B. Toninho, L. Caires, and F. Pfenning. Functions as Session-Typed Processes. FoSSaCS, 7213(Chapter 23):346–360, 2012.
A. S. Troelstra. Lectures on Linear Logic, volume 29 of CSLI Lecture Notes.
Center for the Study of Language and Information, Stanford, California,
1992.
V. T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52–
70, 2012. doi: 10.1016/j.ic.2012.05.002. URL http://dx.doi.org/
10.1016/j.ic.2012.05.002.
P. Wadler. Propositions as sessions. In ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark,
September 9-15, 2012, pages 273–286, 2012a. doi: 10.1145/2364527.
2364568. URL http://doi.acm.org/10.1145/2364527.2364568.
P. Wadler. Propositions as sessions. ICFP, pages 273–286, 2012b.
P. Wadler. Propositions as sessions. Journal of Functional Programming,
24(2-3):384–418, 2014.
N. Yoshida and P.-m. Deniélou. Dynamic multirole session types. POPL,
pages 435–446, 2011.

12

2018/3/1

