Session Types
A kind of type discipline for ensuring structured communication/interaction between different parties.
Dyadic Session Types
Dyadic session types control the interaction between two parties. They were introduced by Kohei Honda in the early 1990s: see Honda 1993, Takeuchi 1994.
However, the first highly influential dyadic system of session types was presented at ESOP'98 Honda, Vasconcelos and Kubo 1998. Some important technical work regarding the system in the ESOP'98 paper was carefully covered by Vasconcelos and Yoshida 2007.
Multiparty Session Types
The dyadic session type systems of Honda et al. were generalized to cover multiparty interaction in an asynchronous fashion in a paper at POPL 2008 Honda, Yoshida, and Carbone 2008. A journal version of this paper by the same authors appeared at the Journal of the ACM in 2016.
A technical simplification of Honda-Yoshida-Carbone multiparty session types, as well as a proof of the property of global progress, has appeared in Coppo et al. 2016. That paper also contains an extensive bibliography on multiparty session types.
References
- Some historical references for dyadic session types:
@inproceedings{honda_types_1993,
series = {Lecture {Notes} in {Computer} {Science}},
title = {Types for dyadic interaction},
volume = {715},
doi = {10.1007/3-540-57208-2_35},
booktitle = {{CONCUR}'93},
publisher = {Springer, Berlin, Heidelberg},
author = {Honda, Kohei},
editor = {Best, Eike},
year = {1993},
pages = {509--523}
}
@inproceedings{takeuchi_1994,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {An interaction-based language and its typing system},
volume = {817},
isbn = {978-3-540-58184-0 978-3-540-48477-6},
doi = {10.1007/3-540-58184-7_118},
urldate = {2020-10-12},
booktitle = {{PARLE}'94 {Parallel} {Architectures} and {Languages} {Europe}},
publisher = {Springer Berlin Heidelberg},
author = {Takeuchi, Kaku and Honda, Kohei and Kubo, Makoto},
editor = {Halatsis, Costas and Maritsas, Dimitrios and Philokyprou, George and Theodoridis, Sergios},
year = {1994},
pages = {398--413}
}
- Literature on the Honda-Vasconcelos-Kubo ESOP 1998 system includes:
@inproceedings{honda_1998,
series = {Lecture {Notes} in {Computer} {Science}},
title = {Language primitives and type discipline for structured communication-based programming},
volume = {1381},
url = {http://link.springer.com/10.1007/BFb0053567},
doi = {10.1007/BFb0053567},
booktitle = {Programming {Languages} and {Systems}: {Proceedings} of the 7th {European} {Symposium} on {Programming} ({ESOP}'98)},
publisher = {Springer, Berlin, Heidelberg},
author = {Honda, Kohei and Vasconcelos, Vasco T and Kubo, Makoto},
year = {1998},
pages = {122--138}
}
@article{yoshida_language_2007,
title = {Language {Primitives} and {Type} {Discipline} for {Structured} {Communication}-{Based} {Programming} {Revisited}: {Two} {Systems} for {Higher}-{Order} {Session} {Communication}},
volume = {171},
issn = {15710661},
shorttitle = {Language {Primitives} and {Type} {Discipline} for {Structured} {Communication}-{Based} {Programming} {Revisited}},
doi = {10.1016/j.entcs.2007.02.056},
language = {en},
number = {4},
journal = {Electronic Notes in Theoretical Computer Science},
author = {Yoshida, Nobuko and Vasconcelos, Vasco T.},
year = {2007},
pages = {73--93}
}
- Papers on Honda-Yoshida-Carbone multiparty session types:
@inproceedings{honda_2008,
address = {San Francisco, California, USA},
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 = {ACM Press},
author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
year = {2008}
}
@article{honda_2016,
title = {Multiparty {Asynchronous} {Session} {Types}},
volume = {63},
issn = {0004-5411, 1557-735X},
doi = {10.1145/2827695},
language = {en},
number = {1},
journal = {Journal of the ACM},
author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
month = mar,
year = {2016},
pages = {1--67}
}
@article{coppo_global_2016,
title = {Global progress for dynamically interleaved multiparty sessions},
volume = {26},
issn = {0960-1295, 1469-8072},
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},
file = {Coppo et al. - 2016 - Global progress for dynamically interleaved multip.pdf:C\:\\Users\\tz20861\\Zotero\\storage\\9DT43D6L\\Coppo et al. - 2016 - Global progress for dynamically interleaved multip.pdf:application/pdf}
}
- A survey of session types up until approx. the year 2010 can be found in
@inproceedings{dezani_2010,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Sessions and {Session} {Types}: {An} {Overview}},
volume = {6194},
isbn = {978-3-642-14457-8 978-3-642-14458-5},
shorttitle = {Sessions and {Session} {Types}},
doi = {10.1007/978-3-642-14458-5_1},
urldate = {2020-10-12},
booktitle = {Web {Services} and {Formal} {Methods}},
publisher = {Springer Berlin Heidelberg},
author = {Dezani-Ciancaglini, Mariangiola and de’Liguoro, Ugo},
editor = {Laneve, Cosimo and Su, Jianwen},
year = {2010},
pages = {1--28}
}