并发中的终止问题，重新审视
摘要：序列编程模型中的终止是一个核心属性：如果一个术语的所有规约序列都是有限的，则该术语是终止的。终止在并发编程中也很重要，特别是对于消息传递程序来说。已经开发了多种通过类型实施终止的类型系统。在本文中，我们从终止的统一视角严格比较了几个用于π-演算过程的类型系统。采用会话类型作为参考框架，我们考虑了两种不同的类型系统：一种遵循Deng和Sangiorgi的基于权重的方法，另一种是Caires和Pfenning的线性逻辑与会话类型之间的Curry-Howard对应。我们的技术结果精确地连接了这些非常不同的类型系统，并揭示了它们作为正确的客户/服务器交互类别。
作者：Joseph W. N. Paulus, Jorge A. P''erez, Daniele Nantes-Sobrinho
论文ID：2308.01165
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-03