Tzu-Chun Chen, Mariagniola Dezani-Ciancaglini, Alceste Scala, and Nobuko Yoshida

On The Preciseness of Subtyping in Session Types (Accepted by LMCS, 2017)

This article is the full version of the extended abstract published in PPDP 2014, including detailed definitions and full proofs, which were omitted. In addition, we provide new results about the uniqueness of precise subtyping relations (Corollary 3.5, Theorem 5.10). Moreover, we include a new section (Section 6) dealing with session initialisation and with communication of expressions (including shared channels), which were not treated: this demonstrates that our approach smoothly generalizes to the original calculus, showing that the invariance of shared channel types is precise. 

Sep 09, 2014

Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida

On the Preciseness of Subtyping in Session Types (ACM PPDP 2014)

Subtyping in concurrency has been extensively studied since the early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness has been largely ignored in spite of its usefulness to define the greatest subtyping relation ensuring type safety. This paper formalizes preciseness (i.e. both soundness and complete- ness) of subtyping for mobile processes and studies it for the synchronous and the asynchronous session calculi. We first prove that the well-known session subtyping, the branching-selection subtyping, is sound and complete for the synchronous calculus. Next, we show that in the asynchronous calculus, this subtyping is incomplete for type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but T < S is not derivable by the subtyping. We then propose an asynchronous subtyping system which is sound and complete for the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtypings respecting desired safety properties.

Please reload


T: (+49) 06151-16-27813