Multiparty Asynchronous Session Types
Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review
Standard
Multiparty Asynchronous Session Types. / Honda, Kohei; Yoshida, Nobuko; Carbone, Marco.
In: Journal of the ACM, Vol. 63, No. 1, 9, 2016, p. 1.Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Multiparty Asynchronous Session Types
AU - Honda, Kohei
AU - Yoshida, Nobuko
AU - Carbone, Marco
PY - 2016
Y1 - 2016
N2 - Communication is a central elements in software development. As a potential typed foundation for structured communication-centered programming, session types have been studied over the past decade for a wide range of process calculi and programming languages, focusing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centered applications. Presented as a typed calculus for mobile processes, the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain the friendly type syntax of binary session types while specifying dependencies and capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers and is used as a basis of efficient type-checking through its projection onto individual peers. The fundamental properties of the session type discipline, such as communication safety, progress, and session fidelity, are established for general n-party asynchronous interactions.
AB - Communication is a central elements in software development. As a potential typed foundation for structured communication-centered programming, session types have been studied over the past decade for a wide range of process calculi and programming languages, focusing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centered applications. Presented as a typed calculus for mobile processes, the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain the friendly type syntax of binary session types while specifying dependencies and capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers and is used as a basis of efficient type-checking through its projection onto individual peers. The fundamental properties of the session type discipline, such as communication safety, progress, and session fidelity, are established for general n-party asynchronous interactions.
U2 - 10.1145/2827695
DO - 10.1145/2827695
M3 - Journal article
VL - 63
SP - 1
JO - Journal of the ACM
JF - Journal of the ACM
SN - 0004-5411
IS - 1
M1 - 9
ER -
ID: 83523572