Mixed choice in session types

Journal article

Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the π-calculus where mixed choice was proved more expressive. Recently Casal, Mordido, and Vasconcelos proposed binary session types with mixed choices (CMV⁺ ). Surprisingly, in spite of an inclusion of unrestricted channels with mixed choice, CMV⁺ ’s mixed choice is rather separate and not mixed. We prove this negative result using two methodologies (using either the leader election problem or a synchronisation pattern as distinguishing feature), showing that there exists no good encoding from the π-calculus into CMV⁺ , preserving distribution. We then close their open problem on the encoding from CMV⁺ into CMV (without mixed choice), proving its soundness.

Authors: Peters, K; Yoshida, N

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Information and Computation
• Volume: 298
• Article number: 105164
• Publication date: 2024-03-26
• Acceptance date: 2024-03-21
• DOI: 10.1016/j.ic.2024.105164
• EISSN: 1090-2651
• ISSN: 0890-5401
• Language: English
• Keywords: session types; expressive power; mixed choice