Separation and encodability in mixed choice multiparty sessions - Peters, K; Yoshida, N (Association for Computing Machinery, 2024)
Multiparty session types (MP) are a type discipline for enforcing the structured, deadlock-free communication of concurrent and message-passing programs. Traditional MP 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 paper first proposes a general typing system for a mixed choice synchronous multiparty session calculus, and prove type soundness, communication safety, and deadlock-freedom. Next we compare expressiveness of nine subcalcli of MCMPcalculus by examining their encodability (there exists a good encoding from one to another) and separation (there exists no good encoding from one calculus to another). We prove 8 new encodablity results and 20 new separation results. In summary, MCMP is strictly more expressive than classical multiparty sessions (MP) in [19] and mixed choice in mixed sessions in [8]. This contrasts to the results proven in [8, 50] where mixed sessions [8] do not add any expressiveness to non-mixed fundamental sessions in [64], shedding a light on expressiveness of multiparty mixed choice.