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
|
| Summary: | 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. |
|---|