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: http://dx.doi.org/10.4204/EPTCS.246.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org