Multiparty asynchronous session types
Author(s)
Honda, K
Yoshida, N
Carbone, M
Type
Journal Article
Abstract
Communication is becoming one of the central elements in software development. As a potential typed foundation
for structured communication-centred programming, session types have been studied over the last
decade for a wide range of process calculi and programming languages, focussing 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-centred 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.
for structured communication-centred programming, session types have been studied over the last
decade for a wide range of process calculi and programming languages, focussing 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-centred 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.
Date Issued
2016-03-30
Date Acceptance
2015-09-17
Citation
Journal of the ACM, 2016, 63 (1)
ISSN
0004-5411
Publisher
Association for Computing Machinery (ACM)
Journal / Book Title
Journal of the ACM
Volume
63
Issue
1
Copyright Statement
© ACM, 2016. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Journal of the ACM, {VOL #63, ISS #1, (30 Mar 2016)} http://doi.acm.org/10.1145/2827695
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
Subjects
Science & Technology
Technology
Computer Science, Hardware & Architecture
Computer Science, Information Systems
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
Session types
the pi-calculus
projection
global types
global protocols
progress
OBJECT-ORIENTED LANGUAGES
ORDER MOBILE PROCESSES
PI-CALCULUS
INFORMATION-FLOW
PROGRESS
SYSTEM
CONTRACT
SERVICES
ACCESS
Computation Theory & Mathematics
08 Information And Computing Sciences
Publication Status
Published
Article Number
9