论会话类型中子类型化的精确性
计算机科学中的逻辑
2019-03-14 v3
摘要
自 20 世纪 90 年代初以来，子类型化作为类型理论中最有趣的问题之一，在并发领域得到了广泛研究。子类型化关系的正确性通常被表述为类型安全的可靠性。其反方向，即完备性，尽管对于定义确保类型安全的最大子类型化关系非常有用，却在很大程度上被忽略了。本文形式化了移动进程子类型化的精确性（即同时具备可靠性和完备性），并在同步和异步会话演算中对其进行了研究。我们首先证明，著名的会话子类型化，即分支-选择子类型化，对于同步演算是可靠且完备的。接下来我们表明，在异步演算中，该子类型化对于类型安全是不完备的：即存在会话类型 T 和 S，使得 T 可以安全地被视为 S 的子类型，但 T < S 无法由该子类型化推导得出。随后我们提出了一个对于异步演算可靠且完备的异步子类型化系统。该方法为设计遵循所需安全属性的严格基于通道的子类型化提供了通用指导。同步和异步演算首先仅考虑线性通道，然后扩展至包含会话初始化和表达式通信（包括共享通道）。
引用
@article{arxiv.1610.00328,
title = {On the Preciseness of Subtyping in Session Types},
author = {Tzu-chun Chen and Mariangiola Dezani-Ciancaglini and Alceste Scalas and Nobuko Yoshida},
journal= {arXiv preprint arXiv:1610.00328},
year = {2019}
}