MobilityReadingGroup

Less Is More: Multiparty Session Types Revisited

Alceste SCALAS, Nobuko YOSHIDA

Multiparty Session Types (MPST) are a typing discipline ensuring that a message-passing process implements without errors a given multiparty session protocol. In this paper, we propose a new, generalised MPST theory. Our contribution is fourfold. (1) We reveal that a revision of the theoretical foundations of MPST is necessary: classic MPST have a limited subject reduction property, with inherent restrictions that are easily overlooked, and in previous work have led to flawed type safety proofs; our new theory removes such restrictions and fixes such flaws. (2) We contribute a new MPST theory that is less complicated, and yet more general, than the classic one: it does not require global multiparty session types nor binary session type duality — instead, it is grounded on general behavioural type-level properties, and proves type safety of many more protocols and processes. (3) We produce a detailed analysis of type-level properties, showing how, in our new theory, they allow to ensure decidability of type checking, and statically guarantee that processes enjoy, e.g., deadlock-freedom and liveness at run-time. (4) We show how our new theory can integrate type and model checking: type-level properties can be expressed in modal μ-calculus, and verified with well-established tools.

@inproceedings{SY2019,
  author = {Alceste Scalas and Nobuko Yoshida},
  title = {{Less Is More: Multiparty Session Types Revisited}},
  booktitle = {46th ACM SIGPLAN Symposium on Principles of Programming Languages},
  volume = {3},
  pages = {30:1--30:29},
  publisher = {ACM},
  year = 2019
}

@inproceedings{SY2019,
  author = {Alceste Scalas and Nobuko Yoshida},
  title = {{Less Is More: Multiparty Session Types Revisited}},
  booktitle = {46th ACM SIGPLAN Symposium on Principles of Programming Languages},
  volume = {3},
  pages = {30:1--30:29},
  publisher = {ACM},
  doi = "10.1145/3290343",
  year = 2019
}