Synchronous Forwarders

TL;DR

This paper introduces synchronous forwarders, a generalization of arbiters in session types, establishing a logical correspondence with coherence proofs in linear logic, thus advancing the understanding of multiparty communication protocols.

Contribution

It generalizes arbiters to synchronous forwarders and proves their equivalence to coherence proofs in a logic based on linear logic, enriching protocol modeling.

Findings

Synchronous forwarders form a logic with cut elimination.

They characterize coherence in multiparty session types.

Every coherence proof corresponds to a synchronous forwarder.

Abstract

Session types are types for specifying protocols that processes must follow when communicating with each other. Session types are in a propositions-as-types correspondence with linear logic. Previous work has shown that a multiparty session type, a generalisation of session types to protocols of two or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality. And, protocols expressed as coherence can be simulated by arbiters, processes that act as a middleware by forwarding messages according to the given protocol. In this paper, we generalise the concept of arbiter to that of synchronous forwarder, that is a processes that implements the behaviour of an arbiter in several different ways. In a propositions-as-types fashion, synchronous forwarders form a logic equipped with cut elimination which is a special restriction of classical linear logic. Our main result shows that synchronous forwarders are a characterisation of coherence, i.e., coherence proofs can be transformed into synchronous forwarders and, viceversa, every synchronous forwarder corresponds to a coherence proofs.