Less is more revisited: association with global multiparty session types
Multiparty session types (MPST) [12] provide a type discipline where a programmer or architect specifies a whole view of communications as a global protocol, and each distributed program is locally type-checked against its end-point projection. After 10 years from the birth of MPST, Scalas and Yoshi...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Book section |
| Language: | English |
| Published: |
Springer
2024
|
| _version_ | 1817930773587558400 |
|---|---|
| author | Yoshida, N Hou, P |
| author2 | Cavalcanti, A |
| author_facet | Cavalcanti, A Yoshida, N Hou, P |
| author_sort | Yoshida, N |
| collection | OXFORD |
| description | Multiparty session types (MPST) [12] provide a type discipline where a programmer or architect specifies a whole view of communications as a global protocol, and each distributed program is locally type-checked against its end-point projection. After 10 years from the birth of MPST, Scalas and Yoshida [18] discovered that the proofs of type safety in the literature which use the end-point projection with mergeability are flawed. After this paper, researchers wrongly believed that the end-point projection (with mergeability) was unsound. We correct this misunderstanding, proposing a new general proof technique for type soundness of multiparty session π-calculus, which uses an association relation between a global type and its end-point projection. |
| first_indexed | 2024-09-25T04:20:15Z |
| format | Book section |
| id | oxford-uuid:40748363-1ccd-4bdd-a732-2f4912c147ad |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-12-09T03:11:27Z |
| publishDate | 2024 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:40748363-1ccd-4bdd-a732-2f4912c147ad2024-10-15T08:31:29ZLess is more revisited: association with global multiparty session typesBook sectionhttp://purl.org/coar/resource_type/c_1843uuid:40748363-1ccd-4bdd-a732-2f4912c147adEnglishSymplectic ElementsSpringer2024Yoshida, NHou, PCavalcanti, ABaxter, JMultiparty session types (MPST) [12] provide a type discipline where a programmer or architect specifies a whole view of communications as a global protocol, and each distributed program is locally type-checked against its end-point projection. After 10 years from the birth of MPST, Scalas and Yoshida [18] discovered that the proofs of type safety in the literature which use the end-point projection with mergeability are flawed. After this paper, researchers wrongly believed that the end-point projection (with mergeability) was unsound. We correct this misunderstanding, proposing a new general proof technique for type soundness of multiparty session π-calculus, which uses an association relation between a global type and its end-point projection. |
| spellingShingle | Yoshida, N Hou, P Less is more revisited: association with global multiparty session types |
| title | Less is more revisited: association with global multiparty session types |
| title_full | Less is more revisited: association with global multiparty session types |
| title_fullStr | Less is more revisited: association with global multiparty session types |
| title_full_unstemmed | Less is more revisited: association with global multiparty session types |
| title_short | Less is more revisited: association with global multiparty session types |
| title_sort | less is more revisited association with global multiparty session types |
| work_keys_str_mv | AT yoshidan lessismorerevisitedassociationwithglobalmultipartysessiontypes AT houp lessismorerevisitedassociationwithglobalmultipartysessiontypes |