On the preciseness of subtyping in session types

File Description SizeFormat 
preciseness-subtyping.pdfFile embargoed until 01 January 10000618.05 kBAdobe PDF    Request a copy
Title: On the preciseness of subtyping in session types
Author(s): Chen, T-C
Dezani-Ciancaglini, M
Scalas, A
Yoshida, N
Item Type: Journal Article
Abstract: 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 com- pleteness, has been largely ignored in spite of its usefulness to de ne 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 rst 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 6 S is not derivable by the subtyping. We then propose an asynchronous sub- typing 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 rst consid- ered with linear channels only, and then they are extended with session initialisations and communications of expressions (including shared channels).
Publication Date: 1-Jan-2017
Date of Acceptance: 2-Oct-2016
URI: http://hdl.handle.net/10044/1/43231
ISSN: 1860-5974
Publisher: IfCoLog (International Federation of Computational Logic)
Journal / Book Title: Logical Methods in Computer Science
Copyright Statement: This paper is embargoed until publication.
Sponsor/Funder: Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Engineering & Physical Science Research Council (EPSRC)
Funder's Grant Number: ERI 025567 (EP/K034413/1)
PO 1553380
Keywords: 0101 Pure Mathematics
0803 Computer Software
0802 Computation Theory And Mathematics
Publication Status: Accepted
Embargo Date: publication subject to indefinite embargo
Appears in Collections:Computing

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

Creative Commons