Lightening Global Types

TL;DR

This paper introduces a framework for decomposing global session types into lighter versions to eliminate redundant interactions, resulting in clearer communication protocols without losing essential message sequences.

Contribution

It presents a novel method for decomposing global session types into light global types, enhancing clarity and efficiency in communication protocols.

Findings

Reduces redundant interactions in global types

Preserves original interaction sequences

Improves clarity of communication protocols

Abstract

Global session types prevent participants from waiting for never coming messages. Some interactions take place just for the purpose of informing receivers that some message will never arrive or the session is terminated. By decomposing a big global type into several light global types, one can avoid such kind of redundant interactions. Lightening global types gives us cleaner global types, which keep all necessary communications. This work proposes a framework which allows to easily decompose global types into light global types, preserving the interaction sequences of the original ones but for redundant interactions.