Partially Typed Multiparty Sessions

TL;DR

This paper introduces a novel type system for multiparty sessions that allows some communications to be ignored, enabling typing of more complex protocols with desirable properties like session fidelity and partial lock-freedom.

Contribution

It presents a new type system for multiparty sessions accommodating ignored communications, expanding the class of typable protocols with proven properties.

Findings

Type system supports ignored communications in multiparty sessions.

Ensures Subject Reduction, Session Fidelity, and partial Lock-freedom.

Includes a sound and complete type inference algorithm.

Abstract

A multiparty session formalises a set of concurrent communicating participants. We propose a type system for multiparty sessions where some communications between participants can be ignored. This allows us to type some sessions with global types representing interesting protocols, which have no type in the standard type systems. Our type system enjoys Subject Reduction, Session Fidelity and "partial" Lock-freedom. The last property ensures the absence of locks for participants with non ignored communications. A sound and complete type inference algorithm is also discussed.