On the preciseness of subtyping in session types


Subtyping in concurrency has been extensively studied since 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 largest subtyping relation ensuring type safety. This paper formalises preciseness (i.e. both soundness and completeness) 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. Both the synchronous and the asynchronous calculus are first considered with linear channels only, and then they are extended with session initialisations and communications of expressions (including shared channels).

Publication DOI: https://doi.org/10.23638/LMCS-13(2:12)2017
Divisions: College of Engineering & Physical Sciences
Funding Information: Key words and phrases: Session types, Subtyping, Completeness, Soundness, the pi-calculus, Type safety, Asynchronous message permutations. ∗ This work was partly supported by the COST Action IC1201 BETTY. . a Tzu-chun Chen was supported by the ERC grant F
Additional Information: © T. Chen, M. Dezani-Ciancaglini, A. Scalas, and N. Yoshida CC Creative Commons
Uncontrolled Keywords: Asynchronous message permutations,Completeness,Session types,Soundness,Subtyping,The π-calculus,Type safety,Theoretical Computer Science,General Computer Science
Publication ISSN: 1860-5974
Last Modified: 27 Jun 2024 10:06
Date Deposited: 19 Aug 2019 08:06
Full Text Link:
Related URLs: http://www.scop ... tnerID=8YFLogxK (Scopus URL)
https://lmcs.ep ... iences.org/3752 (Publisher URL)
PURE Output Type: Article
Published Date: 2017-06-30
Accepted Date: 2017-06-01
Authors: Chen, Tzu Chun
Dezani-Ciancaglini, Mariangiola
Scalas, Alceste (ORCID Profile 0000-0002-1153-6164)
Yoshida, Nobuko



Version: Published Version

License: Creative Commons Attribution

| Preview

Export / Share Citation


Additional statistics for this record