异步会话子类型化的有效算法及其实现
摘要：会话类型是一种用于分布式系统中端点之间通信的类型,最近已经被整合到主流编程语言中。在实践中，处理这种类型的一个非常重要的概念是子类型，因为它允许为更大类的系统进行类型，其中程序的行为不是精确的预期行为，但是相似。然而，最近的研究表明，在异步设置中的会话类型的子类型判断是不可判定的。为了应对这个负面结果，我们目前所知的方法要么限制会话类型的语法，要么限制通信（考虑有限的异步形式）。两种方法在实践中都太过严格，因此我们通过提出一种检查子类型的算法来采取不同的方法，这个算法是有根据的，但不完整（在某些情况下，它在不返回决定性判断的情况下终止）。该算法基于异步子类型的共归定义的树表示;这个树可能是无限的，算法检查无限成功子树的有限证人的存在。此外，我们提供了一个实现我们算法的工具。我们使用这个工具在许多用以前的方法无法处理的示例上测试我们的算法，并对算法的时间和空间成本进行经验评估。
作者：Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, Gianluigi Zavattaro
论文ID：1907.00421
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22