Session types define protocols that processes must follow when communicating. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic. In previous work, we have shown that the generalization to multiparty session types can be expressed either by coherence proofs or by arbiters, processes that act as middleware by forwarding messages according to the given protocol. In this paper, following the propositions-as-types fashion, we generalize arbiters to a logic, which we call forwarder logic, a fragment of classical linear logic still satisfying cut-elimination. Our main result is summarized as follows: forwarders generalize coherence and give an elegant proof-theoretic characterization of multiparty compatibility, a property of concurrent systems guaranteeing that all sent messages are eventually received and no deadlock ever occurs.

翻译：会话类型定义了沟通过程中必须遵循的程序协议。双会话类型的特殊案例,即双方协议的描述类型,众所周知,是用线性逻辑的一模一样的对应形式。在以往的工作中,我们已经表明,多会话类型的一般化可以通过一致性证据或仲裁者来表达,这些过程可以按照特定协议作为中间软件,通过传递信息来发挥作用。在本文中,我们按照“一式”的方式,将仲裁者概括为逻辑,我们称之为远端逻辑,经典线性逻辑的碎片仍然可以满足截断。我们的主要结果总结如下:先行者将一致性普遍化,并给多会话兼容性提供优雅的证据和理论特征,一种并行系统特性,保证最终收到所有发送的信息,而不会陷入僵局。