March 2016 | KOHEI HONDA, Queen Mary University of London; NOBUKO YOSHIDA, Imperial College London; MARCO CARBONE, IT University of Copenhagen
This paper introduces a new theory of multiparty asynchronous session types, extending the existing binary session type theory to handle interactions among multiple peers. The authors propose a typed calculus for mobile processes, where interactions involving multiple peers are abstracted as global scenarios. Global types retain the syntax of binary session types while specifying dependencies and capturing complex causal chains of multiparty asynchronous interactions. A global type serves as a shared agreement among communication peers and is used for efficient type-checking through its projection onto individual peers. The paper establishes fundamental properties of the session type discipline, such as communication safety, progress, and session fidelity, for general $n$-party asynchronous interactions. The work is motivated by practical communication-centered applications, including business protocols and web services, and provides a formal foundation for designing and validating communication-based systems.This paper introduces a new theory of multiparty asynchronous session types, extending the existing binary session type theory to handle interactions among multiple peers. The authors propose a typed calculus for mobile processes, where interactions involving multiple peers are abstracted as global scenarios. Global types retain the syntax of binary session types while specifying dependencies and capturing complex causal chains of multiparty asynchronous interactions. A global type serves as a shared agreement among communication peers and is used for efficient type-checking through its projection onto individual peers. The paper establishes fundamental properties of the session type discipline, such as communication safety, progress, and session fidelity, for general $n$-party asynchronous interactions. The work is motivated by practical communication-centered applications, including business protocols and web services, and provides a formal foundation for designing and validating communication-based systems.