异步多方协同性的逻辑解释
摘要：会话类型是用于确定并发系统中通信进程必须遵循的协议的类型。在组合两个或更多良好类型化的过程时，会话类型系统必须检查这些过程是否是多方兼容的，这个属性保证所有发送的消息最终都会被接收到，并且永远不会发生死锁。先前的工作已经表明，对偶性和更一般的一致性概念是保证多方兼容性属性的足够语法条件。在本文中，我们按照以命题为类型的方式，将会话类型与线性逻辑联系起来，将一致性推广为转发器。转发器是根据给定协议转发消息的过程，充当中间件。我们的主要结果表明，转发器不仅推广了一致性，还完全捕捉到了所有良好类型化的多方兼容进程。
作者：Marco Carbone and Sonia Marin and Carsten Sch"urmann
论文ID：2305.16240
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-26