Authors: Ghilezan, Silvia 
Pantović, Jovanka
Prokić, Ivan
Scalas, Alceste
Yoshida, Nobuko
Affiliations: Mathematics 
Title: Precise Subtyping for Asynchronous Multiparty Sessions
Journal: ACM Transactions on Computational Logic
Issue Date: 2022
Rank: ~M21
DOI: 10.1145/3568422
Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T ≤ T′ holds, it is safe to replace an implementation of T′ with an implementation of the subtype T, which may allow for more optimised communication patterns. We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices). We cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. Our session decomposition technique expresses the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.
Publisher: ACM DL

Show full item record


checked on Jun 23, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.