Tzu-chun Chen ; Mariangiola Dezani-Ciancaglini ; Alceste Scalas ; Nobuko Yoshida - On the Preciseness of Subtyping in Session Types

lmcs:3752 - Logical Methods in Computer Science, June 30, 2017, Volume 13, Issue 2 - https://doi.org/10.23638/LMCS-13(2:12)2017
On the Preciseness of Subtyping in Session TypesArticle

Authors: Tzu-chun Chen ; Mariangiola Dezani-Ciancaglini ; Alceste Scalas ; Nobuko Yoshida

    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 lin ear channels only, and then they are extended with session initialisations and c ommunications of expressions (including shared channels).


    Volume: Volume 13, Issue 2
    Published on: June 30, 2017
    Accepted on: June 30, 2017
    Submitted on: June 30, 2017
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Turtles: Protocol-Based Foundations for Distributed Multiagent Systems; Funder: UK Research and Innovation; Code: EP/N027833/1
    • Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems; Funder: UK Research and Innovation; Code: EP/L00058X/1
    • Lightweight Verification of Software; Funder: European Commission; Code: 617805
    • Scalable Hybrid Variability for Distributed Evolving Software Systems; Funder: European Commission; Code: 644298
    • From Inherent Concurrency to Massive Parallelism through Type-based Optimizations; Funder: European Commission; Code: 612985
    • From Data Types to Session Types---A Basis for Concurrency and Distribution; Funder: UK Research and Innovation; Code: EP/K034413/1
    • Conversation-Based Governance for Distributed Systems by Multiparty Session Types; Funder: UK Research and Innovation; Code: EP/K011715/1
    • REfactoring Parallel Heterogeneous Resource-Aware Applications - a Software Engineering Approach; Funder: European Commission; Code: 644235

    Publications

    IsCitedBy
    Session Subtyping and Multiparty Compatibility Using Circular Sequents
    • 1 ScholeXplorer

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1710 times.
    This article's PDF has been downloaded 466 times.