Less is more: multiparty session types revisited
File(s)popl19main-p52-p.pdf (1.05 MB)
Published version
Author(s)
Scalas, A
Yoshida, N
Type
Conference Paper
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.
Date Issued
2019-01-02
Date Acceptance
2018-11-09
ISSN
2475-1421
Publisher
Association for Computing Machinery
Start Page
30:1
End Page
30:29
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
3
Copyright Statement
© 2019 Copyright held by the owner/author(s). This work is licenced under a Creative Commons Attribution 4.0 International Licence (https://creativecommons.org/licenses/by/4.0/)
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20131167
EP/L00058X/1, PO 20131167
EP/K011715/1
EP/N027833/1
20103649
Source
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
Publication Status
Published
Start Date
2019-01-13
Finish Date
2019-01-19
Coverage Spatial
Cascais, Portugal