On the expressiveness of mixed choice sessions
File(s)
Published version
Author(s)
Peters, Kirstin
Yoshida, Nobuko
Type
Conference Paper
Abstract
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.
Date Issued
2022-09-12
Date Acceptance
2022-08-05
Citation
Electronic Proceedings in Theoretical Computer Science, EPTCS, 2022, 368, pp.113-130
ISSN
2075-2180
Publisher
Open Publishing Association
Start Page
113
End Page
130
Journal / Book Title
Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume
368
Copyright Statement
© K. Peters and N. Yoshida. This work is licensed under the
Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/)
Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/)
License URL
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
The National Cyber Security Centre (NCSC)
Grant Number
EP/T006544/1
EP/K011715/1
ERI 025567 (EP/K034413/1)
PO 20131167
EP/L00058X/1, PO 20131167
EP/N027833/1
PO 20287680
EP/T014709/1
EP/V000462/1
PO 20293625
4227614
Source
EXPRESS/SOS 2022 : Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics
Publication Status
Published
Start Date
2022-09-12
Coverage Spatial
Warsaw, Poland