Scalas, Alceste and Yoshida, Nobuko (2019). Less is more: multiparty session types revisited. Proceedings of the ACM on Programming Languages, 3 (POPL),
Abstract
Multiparty Session Types (MPST) are a typing discipline ensuring that a message-passing process implements a multiparty session protocol, without errors. In this paper, we propose a new, generalised MPST theory. Our contribution is fourfold. (1) We demonstrate that a revision of the theoretical foundations of MPST is necessary: classic MPST have a limited subject reduction property, with inherent restrictions that are easily overlooked, and in previous work have led to flawed type safety proofs; our new theory removes such restrictions and fixes such flaws. (2) We contribute a new MPST theory that is less complicated, and yet more general, than the classic one: it does not require global multiparty session types nor binary session type duality — instead, it is grounded on general behavioural type-level properties, and proves type safety of many more protocols and processes. (3) We produce a detailed analysis of type-level properties, showing how, in our new theory, they allow to ensure decidability of type checking, and statically guarantee that processes enjoy, , deadlock-freedom and liveness at run-time. (4) We show how our new theory can integrate type and model checking: type-level properties can be expressed in modal µ-calculus, and verified with well-established tools.
Publication DOI: | https://doi.org/10.1145/3290343 |
---|---|
Additional Information: | This work is licensed under a Creative Commons Attribution 4.0 International License. © 2019 Copyright held by the owner/author(s). |
Last Modified: | 06 Aug 2024 08:26 |
Date Deposited: | 20 Jun 2019 11:40 |
Full Text Link: | |
Related URLs: |
http://dl.acm.o ... 3302515.3290343
(Publisher URL) |
PURE Output Type: | Article |
Published Date: | 2019-01-02 |
Accepted Date: | 2019-01-01 |
Authors: |
Scalas, Alceste
(![]() Yoshida, Nobuko |