Multiparty Session Types: Separation and Encodability Results

Multiparty Session Types: Separation and Encodability Results Nobuko Yoshida September 2025 The talk first introduces the history and background of types for communications and multiparty session types, relating to the history of Computer Science in Oxford. Multiparty session types (MPST) are a type discipline for enforcing the structured, deadlockfree communication of concurrent and message-passing programs. Traditional MPST have a limited form of choice in which alternative communication possibilities are offered by a single participant and selected by another. Mixed choice multiparty session types (MCMP) extend the choice construct to include both selections and offers in the same choice. This talk presents a mixed choice synchronous multiparty session calculus and its typing system, which guarantees communication safety and deadlock-freedom. We then discuss the expressiveness of nine subcalculi of the MCMP-calculus by examining: •Encodability: whether a good encoding exists from one calculus to another. •Separation: whether no good encoding exists from one calculus to another. The highlight is that binary (2-party) mixed sessions by Casal et al. (2022) are strictly less expressive than the MCMP-calculus. Joint work with Kirstin Peters, appeared in LICS’24: https://arxiv.org/abs/2405.08104 1