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

@inproceedings{abs-2405-08104,
  title = {Separation and Encodability in Mixed Choice Multiparty Sessions},
  author = {Kirstin Peters and Nobuko Yoshida},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662085}
}