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 -calculus into standard linear -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. Importantly for
distributed applications, it preserves the choreographic nature of MPST and illuminates that
multiparty sessions (and their safety properties) can be precisely represented with a decomposition
into binary linear channels. Previous works have only studied the relation between (limited)
multiparty sessions and binary sessions by orchestration means.
We exploit these results to implement an automated generation of Scala APIs for multiparty
sessions. These APIs act as a layer on top of existing libraries for binary communication channels:
this allows distributed multiparty systems to be safely implemented over binary transports, as
commonly found in practice. Our implementation is also the first to support distributed multiparty
delegation: our encoding yields it for free, via existing mechanisms for binary delegation.