Publications

BibTex format

@inproceedings{Peters:2022:10.4204/EPTCS.368.7,
author = {Peters, K and Yoshida, N},
doi = {10.4204/EPTCS.368.7},
pages = {113--130},
publisher = {Open Publishing Association},
title = {On the expressiveness of mixed choice sessions},
url = {http://dx.doi.org/10.4204/EPTCS.368.7},
year = {2022}
}

Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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 pi-calculus where the mixed choices are proved more expressive than the (non-mixed) guarded choices. To account this issue, recently Casal, Mordido, and Vasconcelos proposed the binary session types with mixed choices (CMV+). This paper carries a surprising, unfortunate result on CMV+: 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 pi-calculus into CMV+, preserving distribution. We then close their open problem on the encoding from CMV+ into CMV (without mixed choice), proving its soundness and thereby that the encoding is good up to coupled similarity.
AU  - Peters,K
AU  - Yoshida,N
DO  - 10.4204/EPTCS.368.7
EP  - 130
PB  - Open Publishing Association
PY  - 2022///
SN  - 2075-2180
SP  - 113
TI  - On the expressiveness of mixed choice sessions
UR  - http://dx.doi.org/10.4204/EPTCS.368.7
UR  - http://hdl.handle.net/10044/1/99693
ER  -

Download

ProfessorNobukoYoshida

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)