On the preciseness of subtyping in session types
File(s)1610.00328.pdf (644 KB)
Published version
Author(s)
Chen, T-C
Dezani-Ciancaglini, M
Scalas, A
Yoshida, N
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).
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).
Date Issued
2017-06-30
Date Acceptance
2016-10-02
Citation
Logical Methods in Computer Science, 2017, 13 (2)
ISSN
1860-5974
Publisher
IfCoLog (International Federation of Computational Logic)
Journal / Book Title
Logical Methods in Computer Science
Volume
13
Issue
2
Copyright Statement
This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany
License URL
Sponsor
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)
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
EP/N027833/1
Subjects
Science & Technology
Technology
Computer Science, Theory & Methods
Logic
Computer Science
Science & Technology - Other Topics
Session types
Subtyping
Completeness
Soundness
the pi-calculus
Type safety
Asynchronous message permutations
PI-CALCULUS
LANGUAGE PRIMITIVES
COMMUNICATION
POLYMORPHISM
DISCIPLINE
PROGRESS
0101 Pure Mathematics
0803 Computer Software
0802 Computation Theory And Mathematics
Publication Status
Published
Article Number
3752