Multiparty Sessions based on Proof Nets
Dimitris Mostrous
LaSIGE, Department of Informatics, Faculty of Engineering
University of Lisbon, Portugal.
dimitris@di.fc.ul.pt

We interpret Linear Logic Proof Nets in a term language based on Solos calculus. The system
includes a synchronisation mechanism, obtained by a conservative extension of the logic, that enables
to define non-deterministic behaviours and multiparty sessions.

1

Introduction

Since their inception, sessions [11, 19] and multiparty sessions [12] have been gaining momentum as a
very useful foundation for the description and verification of structured interactions. Interestingly, recent
works have established a close correspondence between typed, synchronous pi-calculus processes and
sequent proofs of a variation of Intuitionistic Linear Logic [3]. This particular interpretation of Linear
proofs is considered a sessions system because it has (for practical purposes) the same type constructors but with a clear logical motivation. In this paper we outline a system based on an interpretation of
the proof objects of Classical Linear Logic, namely Proof Nets [8], improving our previous work [16].
The process language resembles Solos [14] and exhibits asynchrony in both input and output. Proof
Nets have a number of advantages over sequent proofs, such as increased potential for parallelism and
a very appealing graphical notation that could be seen as a new kind of global type [12]. Nevertheless,
accurate logical interpretations are typically deterministic, which limits their applicability to concurrent
programming. However, with a very modest adaptation that enables synchronisation, non-deterministic
behaviours can be allowed without compromising the basic properties of interest, namely strong normalisation and deadlock-freedom.
Let us distinguish multiparty behaviours and the multiparty session types (global types) of [12].
A multiparty behaviour emerges when more than two processes can be part of the same session, and
this is achieved at the operational level by a synchronisation mechanism such as the multicast request
a[2..n](~s).P [12]. We propose a similar mechanism in the form of replications with synchronisation,
!a1 (x1 ) · · · an (xn ).P, which allow a service to be activated with multiple parties. A global type captures
the interactions and sequencing constraints of the complete protocol of a program. In our proposal, the
equivalent to a global type is the proof net of the program. Although our approach is technically very
different, we believe that the logical foundations and simpler meta-theory are appealing. We show how
pi-calculus channels with i/o type and a multi-party interaction from [12] can be encoded.

2

The Process Interpretation

Syntax The language is inspired by proof nets except that connectives have explicit locations (names).
Types are ranged over by A, B,C, with type variables ranging over X, Y. We assume a countable set of
names, ranged over by a, b, c, x, y, z, r, k. Then, e
b stands for a sequence b1 , . . . , bn of length |e
b| = n, and
Alastair F. Donaldson, Vasco Vasconcelos (Eds.): Proceedings
of the 7th Workshop on Programming Language Approaches
to Concurrency and Communication-cEntric Software (PLACES 2014)
EPTCS 155, 2014, pp. 1–8, doi:10.4204/EPTCS.155.1

c D. Mostrous
This work is licensed under the Creative Commons
Attribution-Noncommercial License.

2

Multiparty Sessions based on Proof Nets

similarly for types. Processes, P, Q, R, are defined as follows:
e xe)
P ::= a(A,
ab

e ye)
a(X,

a / i(b)

a . {i(xi :Ai ).Pi }i∈I

?a(b)

!ai (xi :Ai )i∈I .P

X 7→ A

(νa:A)P

(νX)P

(P | Q)

0

e ye) and a(A,
e xe). In typed processes,
There are two kinds of solos-like [14] communication devices: a(X,
1
we will be using the nullary signals a for a() and a for a(), the binary input a(b, c) (resp. output
a(b, c)) and the asynchronous polymorphic input a(X, b) (resp. output a(B, b)). The explicit substitution,
ab, interprets Linear Logic axioms; this is standard in related works [16, 2]. The type alias X 7→ A
is simply a typing device, and the scope of X is restricted with (νX)P. The branching connective a .
{i(xi :Ai ).Pi }i∈I , with I = {1, . . . , n}, written also in the form a . {1(x1 :A1 ).P1 8 · · · 8 n(xn :An ).Pn }, offers
an indexed sequence of alternative behaviours. One of these can be selected using a / k(b) with k ∈ I. Our
notion of replication enables synchronisation, similarly to a multiparty “accept” (cf. [12]). The notation
is !ai (xi :Ai )i∈I .P, written also as !a1 (x1 :A1 ) · · · an (xn :An ).P with n ≥ 1. Dually, ?a(b) can be thought as a
“request.”
Free, passive, and active names The free names (fn(P)) are defined in the standard way. We just note
that the only bound names are a in (νa:A) P and the xi in a . {i(xi :Ai ).Pi }i∈I and !ai (xi :Ai )i∈I .P. The
passive names (pn(P)) are defined similarly to fn(P) except for:
e xe)) = pn(a(A,
e xe)) = {e
pn(a(X,
x}
pn(a / i(b)) = pn(?a(b)) = {b}
pn(ab) = 0/
pn(a . {i(xi :Ai ).Pi }i∈I ) = ∪i∈I (pn(Pi ) \ {xi })
pn(!ai (xi :Ai )i∈I .P) = pn(P) \ ∪i∈I {xi }

The active names (an(P)) are defined by an(P) = fn(P) \ pn(P). For example, y in (νx)( a(x, y) | xy ) is
not active. (As usual, we assume the name convention.)
Structure Equivalence With ≡ we denote the least congruence on processes that is an equivalence relation, equates processes up to α-conversion, satisfies the abelian monoid laws for parallel composition,
the usual laws for scope extrusion, and satisfies the following axioms:2
(νX)0 ≡ 0

(νX)P | Q ≡ (νX)( P | Q ) (X 6∈ ftv(Q))

(νX)(νY)P ≡ (νY)(νX)P
ab ≡ ba

(νX)(νa:A)P ≡ (νa:A)(νX)P

(X 6∈ ftv(A))

ab | !a1 (x1 :A1 ) · · · a(x:A) · · · an (xn :An ).P ≡ ab | !a1 (x1 :A1 ) · · · b(x:A) · · · an (xn :An ).P

The most notable axiom is the last one, which effects a forwarding, e.g., ?a(x) | ab | !b(y).P ≡2 ab | ?a(x) | !a(y).P.
As can be seen next, the term on the right can now reduce.
Reduction “−→” is the smallest binary relation on terms such that:
e xe) −→ X^
e ye) | a(X,
e
a(A,
7→ A | xy
a / k(b) | a . {i(xi :Ai ).Pi }
−→ Pk {b/x }

e |e
e = |X|,
|A|
x| = |e
y|

(R-Com)

k∈I
(R-Sel)
k
b
(R-Sync)
∏i∈I ?ai (bi ) | !ai (xi :Ai )i∈I .P −→ P{ i /xi }i∈I | !ai (xi :Ai )i∈I .P
(νa:A)( ab | P ) −→ P{b/a}
a 6= b, a ∈ an(P)
(R-Ax)
i∈I

P ≡ P0 −→ Q0 ≡ Q ⇒ P −→ Q
Contexts in (R-Ctx) :

(R-Str)

P −→ Q ⇒ C[ P ] −→ C[ Q ] (R-Ctx)

C[ · ] ::= · | ( C[ · ] | P ) | (νa : A) C[ · ] | (νX) C[ · ]

1 They

have no computational content, but without them reduction leaves garbage axioms of unit type.
noting that ftv((νX)P) = ftv(P) \ X. The free type variables
of a type A (ftv(A)) are also standard and arise from ∀/∃.
2 The free type variables (ftv(P)) are defined in a standard way,

D. Mostrous

3

(R-Com) resembles solos reduction [14] but with explicit fusions [7, 16]. Specifically, given two
e stands for x1 y1 | · · · | xn yn or 0 if the vectors are empty. For
vectors xe and ye of length n, the notation xy
polymorphism we create type aliases: X^
7→ A stands for X1 7→ A1 | · · · | Xn 7→ An . Combined type and
name communication appears also in a synchronous setting [18]. (R-Sel) is standard. In (R-Sync) we
synchronise on all ai , obtaining a form of multi-party session against ?a1 (b1 ) | · · · | ?an (bn ). (R-Ax)
effects a capture-avoiding name substitution, defined in the standard way. The side-condition a 6= b
guarantees that no bound name becomes free; a ∈ an(P) ensures that the cut is applied correctly, that is,
against two (or more) conclusions.
The Caires-Pfenning axiom reduction (R-Ax) is based on (νa)( [a ↔ b] | P ) −→ P{b/a} (a 6= b)
from [17], which is similar to the “Cleanup” rule of [1]. However, in an asynchronous language,
.
this rule breaks subject reduction, which motivates our side-condition a ∈ an(P). For example, Q =
(νx, y)( ahx, yi | [x ↔ b] | [y ↔ c] ) is typable in the system of [5], with conclusion b : A, c : B ` Q ::
a : A ⊗ B, but it reduces to (νy)( ahb, yi | [y ↔ c] ) which is not typable.3
Types and duality The types, ranged over by A, B,C, D. . . , are linear logic formulae [8]:
A ::= 1 ∼ A ⊗ B A ` B A & B A ⊕ B !m A ?m A ∀X.A ∃X.A X ∼X

The mode m can be ε (empty) or ? (synchronising): ε is a formality and is never shown; ? is used
to enforce some restrictions, but does not generally alter the meaning of types. Negation ∼( · ), which
corresponds to duality, is an involution on types (∼(∼A) = A) defined in the usual way (we use the
notation from [10]):
.
.
.
.
∼1 = ∼
∼∼ = 1
∼(A ⊗ B) = ∼A ` ∼B
∼(A ` B) = ∼A ⊗ ∼B
.
.
.
.
∼(A & B) = ∼A ⊕ ∼B
∼(A ⊕ B) = ∼A & ∼B
∼(!m A) = ?m ∼A
∼(?m A) = !m ∼A
.
.
.
∼(∀X.A) = ∃X.∼A
∼(∃X.A) = ∀X.∼A
∼(∼X) = X

The multiplicative conjunction A ⊗ B (with unit 1) is the type of a channel that communicates a name
of type A and a name of type B, offered by disconnected terms; it can be thought as an “output.” The
multiplicative disjunction A ` B (with unit ∼) is only different in that the communicated names can
be offered by one term; this possibility of dependency makes it an “input.” In a standard way, the
additive conjunction A & B is an external choice (branching), and dually additive disjunction A ⊕ B is
an internal choice (selection). Ignoring modes, the exponential types !A and ?A can be understood as a
decomposition of the “shared” type in sessions: !A is assigned to a persistent term that offers A; dually,
?A can be assigned to any name with type A so that it can communicate with !∼A. The second-order
types ∀X.A and ∃X.A are standard, as is type substitution: A[B/X] stands for A with B for X, and ∼B for
∼X.
Judgements and interfaces A judgement P . Γ denotes that term P can be assigned the interface Γ.
Interfaces, ranging over Γ, ∆, are sequences with possible repetition, defined by:
Γ

::=

0/ | Γ, a : A

| Γ, [a : A] | Γ, X

a : A is standard. A discharged occurrence [a : A] indicates that a has been used as A: it serves to protect
linearity, since a can no longer be used. Γ, X records that X appears free in the term, ensuring freshness
e stands for a1 : A1 , . . . , an : An . ?Γ stands for ae: ?A,
f i.e., a1 : ?A1 , . . . , an : ?An .
of type variables. ae: A
e Let fn(a : A) = fn([a : A]) = a and fn(X) = 0,
Similarly, [Γ] means [e
a : A].
/ plus the obvious definition for
3 The reduction rule is not mentioned in [5], but the type rule is given and one of the authors relayed to me that reduction is
assumed to be the same as in [17].

4

Multiparty Sessions based on Proof Nets

(New)
P . Γ, [a : A]
(νa : A)P . Γ
(Ax)
ab . a : A, b : ∼A
(CoMix)
P . Γ, Θ

(NewX)
P . Γ, X
X 6∈ ftv(Γ)
(νX) P . Γ

(Sub)
Γ4∆
P.∆
P.Γ

(Cut)
P . Γ, a : A
Q . ∆, a : ∼A
P | Q . [a : A], Γ, ∆
Q . ∆, Θ
Θ ⊆ {a : ?? A}
P | Q . Γ, ∆, Θ

(Str)
P≡Q
Q.Γ
P.Γ

(OpenCut)
P . Γ, a : !m A
Q . ∆, a : ?m ∼A
P | Q . Γ, ∆, a : !m A
(1)

(∼)

a() . a : 1

P.Γ
a() | P . Γ, a : ∼

(⊗)

(`)

P . Γ, b : A
Q . ∆, c : B
a(b, c) | P | Q . [b : A, c : B], Γ, ∆, a : A ⊗ B

P . Γ, b : A, c : B
a(b, c) | P . [b : A, c : B], Γ, a : A ` B

(⊕1 )

(&)
P . Γ, b : A
Q . Γ, c : B
b, c 6∈ fn(Γ)
a . {1(b:A).P 8 2(c:B).Q} . Γ, a : A & B

P . Γ, b : A
a / 1(b) | P . [b : A], Γ, a : A ⊕ B
(∀)
P . Γ, b : A X 6∈ ftv(Γ)
a(X, b) | P . [b : A], X, Γ, a : ∀X.A

(TyAl)
P[A/X] . Γ
X 7→ A | P . Γ, X

(∃)
P . Γ, b : C
C = A[B/X]
a(B, b) | P . [b : C], Γ, a : ∃X.A

(!)
P . ?Γ, {xi : Ai }i∈I
∀i ∈ I . xi 6∈ fn(?Γ) I 6= 0/ ∀i ≥ 2 . mi = ?
!ai (xi :Ai )i∈I .P . ?Γ, {ai : !mi Ai }i∈I

(?D)
P . Γ, b : A
? a(b) | P . [b : A], Γ, a : ?m A

Figure 1: Linear Logic Typing with Multiparty Promotion
free type variables (ftv(Γ)). We consider well-formed interfaces, in which only a : ?A can appear multiple
times, but a : ?? A cannot. Moreover, (Γ, X) is well-formed when Γ is well-formed and ∃σ .σ (Γ) = [∆], Σ
such that X 6∈ ftv(Σ). For example in the (∀) rule the conclusion is Γ, [x : A], X, a : ∀X.A with X possibly
free in A.
Subtyping The usual structural rules of Linear Logic are incorporated into the relation Γ 4 ∆:
Γ, [a : A] 4 Γ, [a : ∼A]
Γ, a : ?A 4 Γ, a : ?A, a : ?A

Γ 4 σ (Γ)

Γ, a : ?A 4 Γ, a : ?? A

Γ, a : ?m A 4 Γ
Γ, a : !? A 4 Γ, a : !A

The first rule identifies the type of a discharged occurrence and its dual, matching a type annotation
which may be (νa : A) or (νa : ∼A). Then we have exchange, weakening, contraction. The last two
axioms alter the mode: we can forget ? in ?? A, and dually we can record it on !A.
Typing rules can be found in Fig. 1. We type modulo structure equivalence, a possibility suggested
by [15] and used in [3]. This is because associativity of “ | ” does not preserve typability, i.e., a cut
between P and (Q | R) may be untypable as (P | Q) | R; (νa) causes similar problems.
In (Cut) the name a is discharged and can then be closed with (New). (OpenCut) was added for
two reasons. First, it is intuitive, since we are not required to close the name, i.e., to fix the number of
clients of !A, departing from the de facto interpretation of “cut as composition under name restriction.”
.
Second, it is needed for soundness. Take R = (νa : !A)( ab | ? a(x) | P | !a(y).Q ) typed with R . Γ, b : !A.

D. Mostrous

5

Using (R-Ax) we obtain R −→ ?b(x) | P{b/a} | !b(y).Q, which is only typable with the same interface
by using (OpenCut); with (Cut) we obtain Γ, [b : !A].4
Asynchronous messages can encode standard sessions (see [4, 5]): a(b, c) with type A⊗B maps to the
session type !s ∼A.B or !s ∼B.A. Dually, a(x, y) with ∼A ` ∼B maps to ?s ∼A.∼B or ?s ∼B.∼A. To write
processes in standard sessions style, with reuse of names (e.g., ab; a(x); 0), we introduce abbreviations
that use the second component for a’s continuation:
ab; P
a / lk ; P
aB; P

.
=
.
=
.
=

(νx, y)( a(x, y) | xb | P{y/a} )
(νx)( a / k(x) | P{x/a} )
(νx)( a(B, x) | P{x/a} )

a(x); P
a . {li .Pi }i∈I
a(X); P

.
=
.
=
.
=

(νx, y)( a(x, y) | P{y/a} )
a . {i(xi ).Pi {xi /a}}i∈I
(νX, x)( a(X, x) | P{x/a} )

It is easy to check that linear redices commute with all other redices, and therefore a “real” prefix would
not have any effect on computation except to make it more sequential.
The rule (!) implements an extension of the logic:
?Γ, A
?Γ, !A

(promotion)

becomes

?Γ, A1 , . . . , An
?Γ, !A1 , . . . , !An

(multi-promotion)

Actually we need to employ some restrictions on this rule, which is why all conclusions except the first
must have a ?-mode. Since there is no contraction for ?? ,5 all the ai : ?? ∼Ai (i ≥ 2) will come from terms
with just one call to the session.6 The first conclusion, a1 : !m1 A1 , can have standard mode (m1 = ε),
which allows a client’s call with a1 : ?∼A1 to be connected to (i.e., to depend on) other calls on a1 . In
this way we provide a hook for one client to participate in another instance of the same session, and this
facilitates a form of dynamic join. We return to this concept in the first example.
Finally, the sidecondition in (&, !) forbids premises from having multiple copies of a name (e.g.,
x : ?A, x : ?A) which should be removed in the conclusion; essentially it forces contractions (by 4). Other
rules are immune by the well-formedness of Γ, [a : A]7 .
Expressiveness & Properties The system is an extension of proof nets, in process form, so it can encode
System F, inductive sessions (using second-order features), etc. Due to space limitations we only show
two examples: (a) how shared channels can be simulated with synchronisation; (b) the (two Buyer, one
Seller) protocol from [12].
a) channels Non-determinism can be expressed by sharing a channel between multiple competing processes trying to send and receive messages. This is impossible with existing logical sessions systems,
and more generally if we follow the logic “by the book.” A channel a with i/o type (A, ∼A), i.e.,
that exports two complementary capabilities A and ∼A, can be encoded by the two names a1 and a2 in
!a1 (x:A) a2 (y:∼A).xy . a1 : !A, a2 : !? ∼A. The channel is used by terms with a1 : ?∼A or a2 : ?? A, and
there can be multiple instances of each, giving rise to critical (non-deterministic) pairs. Moreover, A can
be linear, i.e., we can communicate linear values through shared channels, which is a novel feature. For
example:
? a1 (b1 ) | ? a2 (b2 ) | ? a2 (b3 ) | !a1 (x:A) a2 (y:∼A).xy | P | R | S
−→(a) b1 b2 | ?a2 (b3 ) | !a1 (x:A) a2 (y:∼A).xy | P | R | S
−→(b) b1 b3 | ?a2 (b2 ) | !a1 (x:A) a2 (y:∼A).xy | P | R | S
4 Several works [17, 5, 20, 2] would not enjoy subject reduction if this example could be transferred: their cut rule requires
(νb)(· · · ), which is here missing. These works don’t have “Mix” (here: (CoMix)), which we used in the example; but this
should be checked, since “Mix” can be encoded with a new conclusion c : ∼ ⊗ ∼ [8, p. 100].
5 More accurately: contraction of ? ∼A is multiplicative.
?
i
6 In the sense that two calls can never depend on each other.
7 It is subtle but due to the variable convention, (&) is actually immune too; the condition serves for clarity.

6

Multiparty Sessions based on Proof Nets

First, note that confluence is lost: assume P, R, S cannot reduce and it becomes obvious. The graphical
notation with a reduction of the first possibility is depicted below.
P

R

b1 : ∼A

x: A
@

a1 : ?∼A

y : ∼A

b2 : A

S

P

b3 : A −→ b1 : ∼A b1 : A

b2 : ∼A

R

S

b2 : A

b3 : A

@

a1 : !A a2 : !? ∼A

a2 : ?? A a2 : ?? A

a2 : ?? A
x: A
@

y : ∼A
@

a1 : !A a2 : !? ∼A

It is possible that P has another call to a1 , but by the restriction on ?? -types there cannot be a “trip” from
b2 to a2 , as this would lead to a cycle. Concretely, if R has another call to a2 , then it is from a part
disconnected to b2 , and similarly for S; see (CoMix).8
b) multiparty interactions The (two Buyer, one Seller) protocol from [12] is shown below, with insignificant adaptations, using the previously explained abbreviations (we omit some signals for 1/∼):
Buyer1
Buyer2

.
=
.
=

Seller

.
=


(νb1 ) ? a1 (b1 ) | b1 “The Art of War”; b1 (quote); (νz)( b1 z; 0 | z quote/2; P1 )

(νb2 ) ? a2 (b2 ) | b2 (quote); b2 (z); z(contrib); b2 / ok; b2 “SW12 3AZ”; b2 (date); P2


x1 (title); x1 e 20; x2 e 20; x1 (z); x2 z;
!a1 (x1 ) a2 (x2 ).
x2 . {ok.x2 (address); x2 “7/Feb”; Q 8 quit.0}

We note that the simplicity of the example has not been sacrificed, compared to the code in [12]. One
difference is that we passed z from Buyer1 to Buyer2 through Seller using x1 (z); x2 z, when in [12] all
names are known to all participants. We do not employ the global types of [12], but there is a proof net
for Buyer1 | Buyer2 | Seller, not shown due to space constraints, and we postulate that:
The proof net can serve as an alternative notion of global type.
Outline of results The expected soundness result for reduction, P . Γ and P −→ P0 implies P0 . Γ, is
obtained in a standard way, but fails without the ?-mode. Strong Normalisation (sN), i.e., P . Γ implies
that all reduction sequences from P are finite, is shown by an adaptation of the reducibility candidates
technique from [8]. The loss of confluence complicates the proof, which is in fact obtained for an
extended (confluent) reduction relation using a technique of [6], from which we derive as a corollary the
result. For sN we prove the (initially) stronger property of reducibility [8], which can also serve as a very
strong progress guarantee.
A Curry-Howard correspondence can be obtained easily for a fragment of the language. For the
multiplicative, additive, and second-order cut-elimination we only need to perform extra axiom cuts (i.e.,
substitutions). For exponentials, we restrict replications to a single input and simulate the actual copying
(with contraction links) that takes place in proof nets with sharing and sequentialised cut-elimination
steps. Indeed, there is still a loss of parallelism compared to standard proof nets, but the term language is more realistic. We show just one case of cut-elimination, the cut (⊗ — `), implemented by
a(b, c) | a(x, y) −→ bx | cy, adding appropriate contexts (P, Q, R):
8 In

general, derelictions can be connected through their premises; try with two copies of a : ?(A ⊕ ∼A).

D. Mostrous

7

P

Q

b: A

c: B

a: A ⊗ B

3

R
x : ∼A

Q

P

y : ∼B −→ c : B b : A

a : ∼A ` ∼B

R
b : ∼A

x : A x : ∼A

c : ∼B

y: B

y : ∼B

Conclusion

We claim that our language is simpler and proof-theoretically more appealing than related works such
as [3]: structured interactions take place as expected (fidelity), but parallelism is not inhibited by the use
of prefix, which cannot anyway alter the result in a deterministic setting. It is really a question of proof
nets vs. sequent proofs, and in logic the first are almost always preferable. Even with synchronisation
and the induced non-determinism, the system we propose retains good properties, for example it seems
to be the first approach to multiparty behaviours that enjoys strong normalisation. Finally, our notion of
proof net as global type seems to be a reasonable solution for logically founded multiparty sessions.
In relation to Abramsky’s interpretation [1], it is close to proof nets with boxes, i.e., to a completely
synchronous calculus. Moreover, it is not so friendly syntactically, it does not have a notion of bound
name, copying of exponentials is explicit (no sharing), and of course it is completely deterministic. An
interesting future direction would be to obtain a light variation of our system, e.g., following [9]. Then
we could speak of implicit complexity for multiparty sessions, similarly to what has been done in [13]
for binary sessions. Due to space restrictions, more examples and all proofs have been omitted. These
will appear in a longer version, see http://www.di.fc.ul.pt/~dimitris/.

References
[1] Samson Abramsky (1993): Computational Interpretations of Linear Logic. Theor. Comput. Sci. 111(1-2),
pp. 3–57. Available at http://dx.doi.org/10.1016/0304-3975(93)90181-R.
[2] Luı́s Caires, Jorge A. Pérez, Frank Pfenning & Bernardo Toninho (2013): Behavioral Polymorphism and
Parametricity in Session-Based Communication. In Matthias Felleisen & Philippa Gardner, editors: ESOP,
Lecture Notes in Computer Science 7792, Springer, pp. 330–349. Available at http://dx.doi.org/10.
1007/978-3-642-37036-6_19.
[3] Luı́s Caires & Frank Pfenning (2010): Session Types as Intuitionistic Linear Propositions. In Paul Gastin &
François Laroussinie, editors: CONCUR, Lecture Notes in Computer Science 6269, Springer, pp. 222–236.
Available at http://dx.doi.org/10.1007/978-3-642-15375-4_16.
[4] Romain Demangeon & Kohei Honda (2011): Full Abstraction in a Subtyped pi-Calculus with Linear Types.
In Joost-Pieter Katoen & Barbara König, editors: CONCUR, Lecture Notes in Computer Science 6901,
Springer, pp. 280–296. Available at http://dx.doi.org/10.1007/978-3-642-23217-6_19.
[5] Henry DeYoung, Luı́s Caires, Frank Pfenning & Bernardo Toninho (2012): Cut Reduction in Linear Logic
as Asynchronous Session-Typed Communication. In Patrick Cégielski & Arnaud Durand, editors: CSL,
LIPIcs 16, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 228–242. Available at http://dx.
doi.org/10.4230/LIPIcs.CSL.2012.228.
[6] Thomas Ehrhard & Olivier Laurent (2010): Interpreting a finitary pi-calculus in differential interaction nets.
Inf. Comput. 208(6), pp. 606–633. Available at http://dx.doi.org/10.1016/j.ic.2009.06.005.

8

Multiparty Sessions based on Proof Nets

[7] Philippa Gardner, Cosimo Laneve & Lucian Wischik (2007): Linear forwarders. Inf. Comput. 205(10), pp.
1526–1550. Available at http://dx.doi.org/10.1016/j.ic.2007.01.006.
[8] Jean-Yves Girard (1987): Linear Logic. Theor. Comput. Sci. 50, pp. 1–102. Available at http://dx.doi.
org/10.1016/0304-3975(87)90045-4.
[9] Jean-Yves Girard (1998): Light Linear Logic. Inf. Comput. 143(2), pp. 175–204. Available at http://dx.
doi.org/10.1006/inco.1998.2700.
[10] Jean-Yves Girard (2011): The Blind Spot. European Mathematical Society. Available at http://dx.doi.
org/10.4171/088.
[11] Kohei Honda, Vasco Thudichum Vasconcelos & Makoto Kubo (1998): Language Primitives and Type Discipline for Structured Communication-Based Programming. In Chris Hankin, editor: ESOP, Lecture Notes in
Computer Science 1381, Springer, pp. 122–138. Available at http://dx.doi.org/10.1007/BFb0053567.
[12] Kohei Honda, Nobuko Yoshida & Marco Carbone (2008): Multiparty asynchronous session types. In
George C. Necula & Philip Wadler, editors: POPL, ACM, pp. 273–284. Available at http://doi.acm.
org/10.1145/1328438.1328472.
[13] Ugo Dal Lago & Paolo Di Giamberardino (2011): Soft Session Types. In Bas Luttik & Frank Valencia,
editors: EXPRESS, EPTCS 64, pp. 59–73. Available at http://dx.doi.org/10.4204/EPTCS.64.5.
[14] Cosimo Laneve & Björn Victor (2003): Solos In Concert. Mathematical Structures in Computer Science
13(5), pp. 657–683. Available at http://dx.doi.org/10.1017/S0960129503004055.
[15] Robin Milner (1992): Functions as Processes. Mathematical Structures in Computer Science 2(2), pp. 119–
141. Available at http://dx.doi.org/10.1017/S0960129500001407.
[16] Dimitris Mostrous (2012): Proof Nets in Process Algebraic Form. Available at http://www.di.fc.ul.
pt/~dimitris/.
[17] Jorge A. Pérez, Luı́s Caires, Frank Pfenning & Bernardo Toninho (2012): Linear Logical Relations for
Session-Based Concurrency. In: ESOP ’12, pp. 539–558. Available at http://dx.doi.org/10.1007/
978-3-642-28869-2_27.
[18] Benjamin C. Pierce & Davide Sangiorgi (2000): Behavioral equivalence in the polymorphic pi-calculus.
Journal of the ACM 47(3), pp. 531–584. Available at http://doi.acm.org/10.1145/337244.337261.
[19] Kaku Takeuchi, Kohei Honda & Makoto Kubo (1994): An Interaction-based Language and its Typing System.
In Constantine Halatsis, Dimitris G. Maritsas, George Philokyprou & Sergios Theodoridis, editors: PARLE,
Lecture Notes in Computer Science 817, Springer, pp. 398–413. Available at http://dx.doi.org/10.
1007/3-540-58184-7_118.
[20] Philip Wadler (2014): Propositions as sessions. J. Funct. Program. 24(2-3), pp. 384–418. Available at
http://dx.doi.org/10.1017/S095679681400001X.

