Global types and event structure semantics for asynchronous multiparty sessions

TL;DR

This paper introduces a novel interpretation of asynchronous multiparty sessions using Flow Event Structures, providing a more permissive global type framework that ensures session properties like progress.

Contribution

It presents a new notion of global types for asynchronous sessions, interpreted as Prime Event Structures, and proves their equivalence when sessions are typable.

Findings

Global types reflect asynchrony more directly than standard types.

Event Structure interpretation of sessions matches that of their global types when typable.

The approach ensures properties like progress in asynchronous multiparty sessions.

Abstract

We propose an interpretation of multiparty sessions with asynchronous communication as Flow Event Structures. We introduce a new notion of global type for asynchronous multiparty sessions, ensuring the expected properties for sessions, including progress. Our global types, which reflect asynchrony more directly than standard global types and are more permissive, are themselves interpreted as Prime Event Structures. The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its global type.