Multiparty session types, beyond duality

Alceste Scalas*, Nobuko Yoshida

*Corresponding author for this work

    Research output: Contribution to journalArticlepeer-review

    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. 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.

    Original languageEnglish
    Pages (from-to)55-84
    Number of pages30
    JournalJournal of Logical and Algebraic Methods in Programming
    Volume97
    Early online date10 Mar 2018
    DOIs
    Publication statusPublished - Jun 2018

    Bibliographical note

    © 2018 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).

    Keywords

    • Concurrency
    • Duality
    • Multiparty session types
    • Process calculi

    Fingerprint

    Dive into the research topics of 'Multiparty session types, beyond duality'. Together they form a unique fingerprint.

    Cite this