Multiparty Session Types

Multiparty Session Types (MPST) are a type system used to describe communication protocols in concurrent and distributed systems. They were introduced in a POPL 2008 paper by Honda, Yoshida, and Carbone.

An MPST describes communication among multiple processes and/or participants by specifying the type and the direction of data exchanged. These communications are given as a sequence of instructions to send and receive messages.

A classic example of the need for multiparty session types is given by the two-buyer protocol.

Metatheory

The metatheory of MPST is somewhat challenging.

In particular, the original POPL 2008 had only limited results on progress.

A modern reconstruction of the original MPST system which supports a 'global' progress theorem was formulated by Coppo et al. 2016.

Implementations

There has been a lot of work on implementing various aspects of multiparty session types within programming languages.

MPSTs form the basis of Scribble, a specification language for communicating protocols.

References

Multiparty Session Types were first introduced in a paper at POPL 2008:

Honda, Kohei, Nobuko Yoshida, and Marco Carbone. 2008. ‘Multiparty Asynchronous Session Types’. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/1328438.1328472. pdf

@inproceedings{honda_2008,
	title = {Multiparty {Asynchronous} {Session} {Types}},
	isbn = {978-1-59593-689-9},
	doi = {10.1145/1328438.1328472},
	booktitle = {Proceedings of the 35th {Annual} {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
	publisher = {Association for Computing Machinery},
	author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
	year = {2008}
}

There is also a journal version of this paper:

Honda, Kohei, Nobuko Yoshida, and Marco Carbone. 2016. ‘Multiparty Asynchronous Session Types’. Journal of the ACM 63 (1): 1–67. https://doi.org/10.1145/2827695. pdf

@article{honda_2016,
	title = {Multiparty {Asynchronous} {Session} {Types}},
	volume = {63},
	doi = {10.1145/2827695},
	number = {1},
	journal = {Journal of the ACM},
	author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
	year = {2016},
	pages = {1--67}
}

A 'rational reconstruction' with a global progress result was presented in

COPPO, MARIO, MARIANGIOLA DEZANI-CIANCAGLINI, NOBUKO YOSHIDA, and LUCA PADOVANI. “Global Progress for Dynamically Interleaved Multiparty Sessions.” Mathematical Structures in Computer Science 26, no. 2 (2016): 238–302. doi:10.1017/S0960129514000188.

@article{coppo_2016,
	title = {Global progress for dynamically interleaved multiparty sessions},
	volume = {26},
	doi = {10.1017/S0960129514000188},
	number = {2},
	journal = {Mathematical Structures in Computer Science},
	author = {Coppo, Mario and Dezani-Ciancaglini, Mariangiola and Yoshida, Nobuko and Padovani, Luca},
	year = {2016},
	pages = {238--302}
}