Separation and encodability in mixed choice multiparty sessions

Conference item

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.

Authors: Peters, K; Yoshida, N

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Association for Computing Machinery
• Host title: LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
• Journal: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
• Article number: 62
• Publication date: 2024-07-08
• Acceptance date: 2024-04-15
• Event title: 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024)
• Event location: Tallinn, Estonia
• Event website: https://lics.siglog.org/lics24/
• Event start date: 2024-07-08
• Event end date: 2024-07-11
• DOI: 10.1145/3661814.3662085
• ISBN: 979-8-4007-0660-8
• Language: English
• Keywords: typing system; concurrency; protocols; expressiveness; pi-calculus; session types; mixed choice