π-calculus, Session Types research at the University of Oxford
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.
@article{PY2024,
author = {Kirstin Peters and Nobuko Yoshida},
title = {{Mixed choice in session types}},
journal = {IC},
volume = {298},
pages = {105164--},
year = 2024
}
@article{PY2024,
author = {Kirstin Peters and Nobuko Yoshida},
title = {{Mixed choice in session types}},
journal = {Information and Computation},
volume = {298},
pages = {105164--},
doi = "10.1016/j.ic.2024.105164",
year = 2024
}