Multiparty asynchronous session types
File(s)
Published version
Author(s)
Honda, Kohei
Yoshida, Nobuko
Carbone, Marco
Type
Report
Abstract
Communication is becoming one of the central elements in software
development. As a potential typed foundation for structured communication-based
programming, session types have been studied over the last decade for a wide
range of process calculi and programming languages, focussing on binary (twoparty)
sessions. This work extends the foregoing theories of binary session types
to multiparty, asynchronous sessions, which often arise in practical communicationcentred
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 a friendly
type syntax of binary session types while 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 and progress are
established for general n-party asynchronous interactions.
development. As a potential typed foundation for structured communication-based
programming, session types have been studied over the last decade for a wide
range of process calculi and programming languages, focussing on binary (twoparty)
sessions. This work extends the foregoing theories of binary session types
to multiparty, asynchronous sessions, which often arise in practical communicationcentred
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 a friendly
type syntax of binary session types while 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 and progress are
established for general n-party asynchronous interactions.
Date Issued
2007-01-01
Citation
Departmental Technical Report: 07/5, 2007, pp.1-75
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
75
Journal / Book Title
Departmental Technical Report: 07/5
Copyright Statement
© 2007 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
07/5