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.We propose a novel MPST theory based on a rely/guarantee typing system, that checks (1)the guaranteed behaviour of the process being typed, and (2) the relied upon behaviour of other processes. Crucially, our theory achieves type safety by enforcing a typing context liveness invariant throughout typing derivations.Unlike “classic” MPST works, our typing system does not depend on global session types, and does not use syntactic duality checks. As a result, our new theory can prove type safety for processes that implement protocols with complex inter-role dependencies, thus sidestepping an intrinsic limitation of “classic” MPST.

@article{SY2018,
  author = {Alceste Scalas and Nobuko Yoshida},
  title = {{Multiparty Session Types, Beyond Duality}},
  journal = {JLAMP},
  volume = {97},
  pages = {55--84},
  publisher = {Elsevier},
  year = 2018
}

@article{SY2018,
  author = {Alceste Scalas and Nobuko Yoshida},
  title = {{Multiparty Session Types, Beyond Duality}},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {97},
  pages = {55--84},
  publisher = {Elsevier},
  doi = "10.1016/j.jlamp.2018.01.001",
  year = 2018
}