On the expressiveness of mixed choice sessions
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 sessi...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Open Publishing Association
2022
|
| _version_ | 1797112258639167488 |
|---|---|
| author | Peters, K Yoshida, N |
| author_facet | Peters, K Yoshida, N |
| author_sort | Peters, K |
| collection | OXFORD |
| description | 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 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 π-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. |
| first_indexed | 2024-03-07T08:21:37Z |
| format | Journal article |
| id | oxford-uuid:69d52a31-3d1f-4c4a-bb5b-f24181cd233a |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:21:37Z |
| publishDate | 2022 |
| publisher | Open Publishing Association |
| record_format | dspace |
| spelling | oxford-uuid:69d52a31-3d1f-4c4a-bb5b-f24181cd233a2024-01-30T11:34:43ZOn the expressiveness of mixed choice sessionsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:69d52a31-3d1f-4c4a-bb5b-f24181cd233aEnglishSymplectic ElementsOpen Publishing Association2022Peters, KYoshida, NSession 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 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 π-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. |
| spellingShingle | Peters, K Yoshida, N On the expressiveness of mixed choice sessions |
| title | On the expressiveness of mixed choice sessions |
| title_full | On the expressiveness of mixed choice sessions |
| title_fullStr | On the expressiveness of mixed choice sessions |
| title_full_unstemmed | On the expressiveness of mixed choice sessions |
| title_short | On the expressiveness of mixed choice sessions |
| title_sort | on the expressiveness of mixed choice sessions |
| work_keys_str_mv | AT petersk ontheexpressivenessofmixedchoicesessions AT yoshidan ontheexpressivenessofmixedchoicesessions |