A Logical Interpretation of Asynchronous Multiparty Compatibility

Session types specify the protocols that communicating processes must follow in a concurrent system. When composing two or more processes, a session typing system must check whether such processes are compatible, i.e., that all sent messages are eventually received and no deadlock ever occurs. After the propositions-as-types paradigm, relating session types to linear logic, previous work has shown that duality, in the binary case, and more generally coherence, in the multiparty case, are sufficient syntactic conditions to guarantee compatibility for two or more processes, yet do not characterise all compatible set of processes.

In this work, we generalise duality/coherence to a notion of forwarder compatibility. Forwarders are specified as a restricted family of proofs in linear logic, therefore defining a specific set of processes that can act as middleware by transfering messages without using them. As such, they can guide a network of processes to execute asynchronously. Our main result establishes forwarder compatibility as a sufficient and necessary condition to fully capture all well-typed multiparty compatible processes.