MobilityReadingGroup

A Very Gentle Introduction to Multiparty Session Types

Nobuko YOSHIDA, Lorenzo GHERI

Multiparty session types (MPST) are a formal specification and verification framework for message-passing protocols without central control: the desired interactions at the scale of the network itself are specified into a session (called global type). Global types are then projected onto local types (one for each participant), which describe the protocol from a local point of view. These local types are used to validate an application through type-checking, monitoring, and code generation. Theory of session types guarantees that local conformance of all participants induces global conformance of the network to the initial global type. This paper provides a very gentle introduction of the simplest version of multiparty session types for readers who are not familiar with session types nor process calculi.

@inproceedings{YG2020,
  author = {Nobuko Yoshida and Lorenzo Gheri},
  title = {{A Very Gentle Introduction to Multiparty Session Types}},
  booktitle = {16th International Conference on Distributed Computing and Internet Technology},
  series = {LNCS},
  volume = {11969},
  pages = {73--93},
  publisher = {Springer},
  year = 2020
}

@inproceedings{YG2020,
  author = {Nobuko Yoshida and Lorenzo Gheri},
  title = {{A Very Gentle Introduction to Multiparty Session Types}},
  booktitle = {16th International Conference on Distributed Computing and Internet Technology},
  series = {LNCS},
  volume = {11969},
  pages = {73--93},
  publisher = {Springer},
  doi = "10.1007/978-3-030-36987-3_5",
  year = 2020
}