Multiparty Asynchronous Session Types

Kohei Honda, Nobuko Yoshida, Marco Carbone

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

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.
Original languageEnglish
Article number9
JournalJournal of the ACM
Volume63
Issue number1
Pages (from-to)1
Number of pages67
ISSN0004-5411
DOIs
Publication statusPublished - 2016

Keywords

  • progress
  • global protocols
  • global types
  • projection
  • the pi-calculus
  • Session types

Fingerprint

Dive into the research topics of 'Multiparty Asynchronous Session Types'. Together they form a unique fingerprint.

Cite this