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).