A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming

Alceste Scalas, Ornela Dardha, Raymond Hu, Nobuko Yoshida

    Research output: Contribution to conferencePaperpeer-review

    21 Citations (Scopus)


    Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages? We address this problem by (1) developing the first encoding of a full-fledged multiparty session pi-calculus into linear pi-calculus, and (2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala. Our encoding is type-preserving and operationally sound and complete. Crucially, it keeps the distributed choreographic nature of MPST, illuminating that the safety properties of multiparty sessions can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty and binary sessions via centralised orchestration means. We exploit these results to implement an automated generation of Scala APIs for multiparty sessions, abstracting existing libraries for binary communication channels. This allows multiparty systems to be safely implemented over binary message transports, as commonly found in practice. Our implementation is the first to support distributed multiparty delegation: our encoding yields it for free, via existing mechanisms for binary delegation.
    Original languageEnglish
    Number of pages31
    Publication statusPublished - 16 Jun 2017
    Event31st European Conference on Object-Oriented Programming (ECOOP 2017). - Universitat Politècnica de Catalunya (UPC), , Barcelona, Spain
    Duration: 18 Jun 201723 Jun 2017


    Conference31st European Conference on Object-Oriented Programming (ECOOP 2017).
    Internet address


    • process calculi, session types, concurrent programming, Scala


    Dive into the research topics of 'A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming'. Together they form a unique fingerprint.

    Cite this