  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.
