ITU

Multiparty Asynchronous Session Types

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-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 JournalJournal articleResearchpeer-review

Harvard

APA

Vancouver

Author

Honda, Kohei ; Yoshida, Nobuko ; Carbone, Marco. / Multiparty Asynchronous Session Types. In: Journal of the ACM. 2016 ; Vol. 63, No. 1. pp. 1.

Bibtex

@article{f154b152abd34f1ea5d5c0825f87ebd4,
title = "Multiparty Asynchronous Session Types",
abstract = "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.",
author = "Kohei Honda and Nobuko Yoshida and Marco Carbone",
year = "2016",
doi = "10.1145/2827695",
language = "English",
volume = "63",
pages = "1",
journal = "Journal of the ACM",
issn = "0004-5411",
publisher = "Association for Computing Machinery",
number = "1",

}

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