2017/04/11 by Alceste Scalas, Nobuko Yoshida
Computer Science · #cs.PL
paper · pdf · doi:10.4204/eptcs.246.7
published as EPTCS 246, 2017, pp. 37-38 · In Proceedings PLACES 2017, arXiv:1704.02418
arxiv created 2017/04/11 · arxiv updated 2017/04/12
Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many "intuitively correct" examples cannot be typed and/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason for these limitations. Then, we outline a novel MPST typing system that removes these restrictions.