Multiparty session types, beyond duality
File(s)DTRS17-4.pdf (340.94 KB)
Published version
Author(s)
Scalas, Alceste
Yoshida, Nobuko
Type
Report
Abstract
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 present a novel MPST typing system that removes these restrictions.
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 present a novel MPST typing system that removes these restrictions.
Date Issued
2017-01-01
Citation
Departmental Technical Report: 17/4, 2017, pp.1-20
Start Page
1
End Page
20
Journal / Book Title
Departmental Technical Report: 17/4
Copyright Statement
© 2017 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
17/4