Session types are types for specifying the protocols that communicating processes must follow in a concurrent system. When composing two or more well-typed processes, a session typing system must check whether such processes are multiparty compatible, a property that guarantees that all sent messages are eventually received and no deadlock ever occurs. Previous work has shown that duality and the more general notion of coherence are sufficient syntactic conditions for guaranteeing the multiparty compatibility property. In this paper, following a propositions-as-types fashion which relates session types to linear logic, we generalise coherence to forwarders. Forwarders are processes that act as middleware by forwarding messages according to a given protocol. Our main result shows that forwarders not only generalise coherence, but fully capture all well-typed multiparty compatible processes.

翻译：会话类型是一种用于指定并发系统中通信进程所必须遵循的协议的类型。当组合两个或多个类型良好的进程时，会话类型系统必须检查这些进程是否满足多方兼容性，该属性保证所有发送的消息最终都会被接收，且永远不会发生死锁。先前的研究表明，对偶性和更一般的相干性是保证多方兼容性属性的充分句法条件。本文遵循将会话类型与线性逻辑关联起来的"命题即类型"范式，将相干性泛化为转发器。转发器是一种充当中间件的进程，根据给定协议转发消息。我们的主要结果表明，转发器不仅泛化了相干性，而且完全捕获了所有类型良好的多方兼容进程。