A. Scalas, N. Yoshida / Journal of Logical and Algebraic Methods in Programming 97 (2018) 55–84
71
ꢂ
ꢂ
S ≡ q&i∈I mi(Si).Si ∀i∈I ꢂ ꢀ Pi ꢁ ꢀ, yi :Si, x:Si ꢃ ꢁ
ꢂ
[T&x]
ꢂ ꢀ x[q] i∈I∪ J {mi(yi).Pi} ꢁ ꢀ, x:S ꢃ ꢁ
ꢂ
ꢂ
S ≡ q⊕i∈I mi(Si).Si k∈I ꢀy ꢀ y:Sk ꢂ ꢀ P ꢁ ꢀ, x:Sk ꢃ ꢁ
[T⊕x]
ꢂ ꢀ x[q]⊕mkꢄy .P ꢁ ꢀy,ꢀ, x:S ꢃ ꢁ
This is because in [T-⊕], by Proposition 5.7 we can omit ꢀy from the rely context of the rightmost premise. Further, since
∗
x:S reduces autonomously (cf. Definition 2.10), in both [T-&] and [T-⊕] the quantification “∀ꢁꢂ, ꢁꢂꢂ : ꢁ → ꢁꢂ and ꢁꢂ, x:S →
ꢂ
∗
ꢂ
ꢁꢂꢂ, x:Si” amounts to “∀ꢁꢂ : ꢁ → ꢁꢂ and ꢁꢂ, x:S → ꢁꢂ, x:Si”; hence, by Lemma 5.6, checking the rightmost premise once
∗
with ꢁ is sufficient to know that it holds ∀ꢁꢂ such that ꢁ → ꢁꢂ.
This shows that in most cases, our rely/guarantee type checking can be simplified, becoming similar to the “classic”
MPST rules.
6. Conclusions and related work
We presented a new multiparty session typing system (Definition 4.5), based on a rely/guarantee typing strategy, and a
liveness invariant on typing contexts (Definition 4.1). Our typing system provides a subject reduction result (Theorem 4.9)
that overcomes the consistency restrictions of “classic” MPST works. By directly exploiting the typing context semantics, our
typing rules provide flexible type checks supporting all protocols projectable from global types, plus various kinds of live
protocols that cannot be projected from any global type (Section 5). As a bonus, the independence from global types means
that our theory is simpler than the “classic” one, in the sense that it does not depend on its syntactic type manipulations
(i.e., the type projection/merging/duality machinery of “classic” MPST, summarised in Appendix A).
Inter-role dependencies Our rely/guarantee typing system allows to prove type safety of processes implementing protocols
with complex inter-role dependencies: this is generally not supported by “classic” MPST, as discussed in Sections 1, 3.4
and 5, and Examples 3.4 and 4.7. In this respect, to the best of our knowledge, the only work with comparable features
is the one by Dezani-Ciancaglini et al. [15]: it provides a “non-classic” MPST theory where processes can only interact
on one session — and this limitation is crucially exploited to type parallel compositions without splitting their typing
context (cf. Table 8, rule [T-SESS]). Their approach directly tracks a global type along process reductions, without introducing
consistency restrictions. However, unlike the present work, Dezani-Ciancaglini et al. [15] do not support multiple sessions
and delegation — and extending their work in that direction appears challenging. Moreover, our approach does not depend
on the existence of global types: therefore, it is arguably simpler (since it only uses local types), and supports protocols for
which no corresponding global type exists, as shown in Section 5.1.
Global types and liveness Our type system does not assume that a session is typed by projecting some global type: it only
(implicitly) requires that a session is typed by a live composition of local session types, by rule [T-ν] (Fig. 3). If needed,
a set of local types can be related to a choreography either via “top-down” projection (Section 3.1), or via “bottom-up”
synthesis (studied, e.g., by Lange and Tuosto [26] and Lange et al. [27]): these concerns are orthogonal to our typing system.
Our Definition 4.1 (liveness) is inspired by (1) the notion of safety for Communicating Finite-State Machines (CFSMs) Brand
and Zafiropulo [8] (no deadlocks, orphan messages, unspecified receptions) and (2) the idea of “multiparty session types
as CFSMs” outlined by Deniélou and Yoshida [14]. In particular, liveness (Definition 4.1) is closely related to the notion of
Multiparty Compatibility for CFSMs, as illustrated in Section 5.1 (proof of Lemma 5.1). Notably, Deniélou and Yoshida [14]
focus on projecting CFSMs and studying their interactions, and do not technically develop the intuition of “CFSMs as types”
into an actual typing system. For this reason, they do not realise that the “classic” MPST theory cannot fully support their
intuition, due to the consistency requirement and the resulting restrictions. Our work provides an actual multiparty session
typing system that sidesteps these limitations, and comes closer to using “CFSMs as types.”
Deadlock freedom Similarly to most previous MPST works, our approach ensures that a typed ensemble of processes inter-
ꢀ
ꢀ
acting on a single session (i.e., a typed (νs)(
does not guarantee deadlock freedom in presence multiple interleaved sessions. This topic is studied by Bettini et al. [5] and
Coppo et al. [12]: as future work, we plan to investigate how to reuse their results in our theory.
P ), with each P only interacting on s[p]) is deadlock-free; however, it
p
p
p∈I
Recursion and duality Various works on binary session types have investigated the subtle interplay between recursion and
duality. Bono and Padovani [7] and Bernardi and Hennessy [3] independently noticed that the “standard” duality proposed by
Honda et al. [20] (corresponding to Definition A.3) does not commute with the unfolding of recursion for non-tail-recursive
types (i.e., with type variables as payloads). An example of such types is μt.⊕m(t).t, similar to our Example 5.3. This implies
that some “safe” process compositions cannot be typed in binary session theories — and this limitation can also be found
in “classic” MPST works, due to their consistency requirement (that is rooted in binary duality, cf. Definition 3.3). To solve
this issue, Bono and Padovani [7] and Bernardi and Hennessy [3] defined a new notion of duality, called complement by
the latter, and further studied by Bernardi et al. [2]. However, [4, Example 5.21] later noticed that even complement does
ꢂ
ꢂ
not commute, e.g., when unfolding μt.μt .&m(t ).t. This issue was later solved by Lindley and Morris [28, Section 5.2]: