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_ | 1811140328908914688 |
|---|---|
| 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-09-25T04:20:15Z |
| publishDate | 2024 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:40748363-1ccd-4bdd-a732-2f4912c147ad2024-08-02T13:40:22ZLess 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 |