摘要：Subtyping in concurrency has been extensively studied since early 1990s asone of the most interesting issues in type theory. The correctness of subtypingrelations has been usually provided as the soundness for type safety. Theconverse direction, the completeness, has been largely ignored in spite of itsusefulness to define the largest subtyping relation ensuring type safety. Thispaper formalises preciseness (i.e. both soundness and completeness) ofsubtyping for mobile processes and studies it for the synchronous and theasynchronous session calculi. We first prove that the well-known sessionsubtyping, the branching-selection subtyping, is sound and complete for thesynchronous calculus. Next we show that in the asynchronous calculus, thissubtyping is incomplete for type-safety: that is, there exist session types Tand S such that T can safely be considered as a subtype of S, but T < S is not derivable bythe subtyping. We then propose an asynchronous subtyping system which is soundand complete for the asynchronous calculus. The method gives a general guidanceto design rigorous channel-based subtypings respecting desired safetyproperties. Both the synchronous and the asynchronous calculus are firstconsidered with lin ear channels only, and then they are extended with sessioninitialisations and c ommunications of expressions (including shared channels).
