一句话：证明同步会话演算中分支-选择子类型既可靠又完备，并构造异步演算下可靠完备的子类型系统。
会话类型中的子类型关系通常只被证明是可靠的，以保类型安全，而其完备性（能否刻画最大安全子类型关系）长期被忽视。本文形式化移动进程子类型的精确性，即同时要求可靠性与完备性，并在同步和异步会话演算中研究。作者证明经典的分支-选择子类型对同步演算可靠且完备；但在异步演算中该关系对类型安全并不完备：存在可安全视为子类型却无法推导的情形。为此提出一个新的异步子类型系统，证明其对异步演算可靠且完备，并给出设计满足安全性质的基于通道子类型的通用指导。演算先限于线性通道，后扩展至会话初始化与表达式通信（含共享通道）。
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).
@article{paperbot155,
title = {On the Preciseness of Subtyping in Session Types},
author = {Tzu-chun Chen and Mariangiola Dezani-Ciancaglini and Alceste Scalas and Nobuko Yoshida},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
year = {2017},
doi = {10.23638/lmcs-13(2:12)2017}
}