Multiparty Session Types, Beyond Duality (Abstract)

Alceste Scalas
(Imperial College London)
Nobuko Yoshida
(Imperial College London)

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.

In Vasco T. Vasconcelos and Philipp Haller: Proceedings Tenth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2017), Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science 246, pp. 37–38.
Published: 8th April 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: