On Global Types and Multi-Party Session

Abstract

Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a liveness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type. In addition to the technical content, we discuss some limitations of our language of global types and provide an extensive comparison with related specification languages adopted in different communities.

Cited by in corpus (14)

• An Abstract Semantics of the Global View of Choreographies
• Asynchronous Sessions with Input Races
• Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
• Global Types for Open Systems
• Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services
• Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types
• Choreography Synthesis as Contract Agreement
• A Typeful Characterization of Multiparty Structured Conversations Based on Binary Sessions
• On Resolving Non-determinism in Choreographies
• Can determinism and compositionality coexist in RML?
• A Session Type System for Asynchronous Unreliable Broadcast Communication
• Can determinism and compositionality coexist in RML? (extended version)
• On the Enactability of Agent Interaction Protocols: Toward a Unified Approach
• Lightening Global Types