Multiparty session types, beyond duality


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. We propose a novel MPST theory based on a rely/guarantee typing system, that checks (1) the guaranteed behaviour of the process being typed, and (2) the relied upon behaviour of other processes. Crucially, our theory achieves type safety by enforcing a typing context liveness invariant throughout typing derivations. Unlike “classic” MPST works, our typing system does not depend on global session types, and does not use syntactic duality checks. As a result, our new theory can prove type safety for processes that implement protocols with complex inter-role dependencies, thus sidestepping an intrinsic limitation of “classic” MPST.

Publication DOI:
Funding Information: This work was partially supported by EPSRC grants EP/K011715/1 , EP/K034413/1 , EP/L00058X/1 , EP/N028201/1 , and EP/N027833/1 . We thank the anonymous reviewers for their valuable comments and suggestions, and Raymond Hu, Julien Lange, and Bernardo Tonin
Additional Information: © 2018 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (
Uncontrolled Keywords: Concurrency,Duality,Multiparty session types,Process calculi,Theoretical Computer Science,Software,Logic,Computational Theory and Mathematics
Publication ISSN: 2352-2216
Last Modified: 30 Apr 2024 07:16
Date Deposited: 01 Jun 2020 12:01
Full Text Link:
Related URLs: http://www.scop ... tnerID=8YFLogxK (Scopus URL)
https://www.sci ... 1487?via%3Dihub (Publisher URL)
PURE Output Type: Article
Published Date: 2018-06
Published Online Date: 2018-03-10
Accepted Date: 2018-01-22
Authors: Scalas, Alceste (ORCID Profile 0000-0002-1153-6164)
Yoshida, Nobuko



Version: Published Version

License: Creative Commons Attribution

| Preview

Export / Share Citation


Additional statistics for this record