MobilityReadingGroup

Multiparty Session Types, Beyond Duality

Alceste SCALAS, Nobuko YOSHIDA

Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many ‘intuitively correct’ examples cannot be typed and/or cannot be proved type-safe.

We illustrate some of these examples, and discuss the reason for these limitations. Then, we present a novel MPST typing system that removes these restrictions.

@inproceedings{SY2017,
  author = {Alceste Scalas and Nobuko Yoshida},
  title = {{Multiparty Session Types, Beyond Duality}},
  booktitle = {10th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software},
  series = {EPTCS},
  volume = {246},
  pages = {37--38},
  publisher = {Open Publishing Association},
  year = 2017
}

@inproceedings{SY2017,
  author = {Alceste Scalas and Nobuko Yoshida},
  title = {{Multiparty Session Types, Beyond Duality}},
  booktitle = {10th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software},
  series = {EPTCS},
  volume = {246},
  pages = {37--38},
  publisher = {Open Publishing Association},
  doi = "10.4204/EPTCS.246.7",
  year = 2017
}