On global types and multi-party sessions

DOI10.2168/LMCS-8(1:24)2012zbMATH Open1238.68026arXiv1203.0780OpenAlexW2626089800MaRDI QIDQ2881091FDOQ2881091

Authors: Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Luca Padovani 

Publication date: 3 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1203.0780

Recommendations

• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Multiparty Asynchronous Session Types
• A calculus of global interaction based on session types
• Multiparty session nets

zbMATH Keywords

type theorysession typessubtypingweb servicesconcurrency theoryglobal types

Mathematics Subject Classification ID

Logic in computer science (03B70) Network design and communication in computer systems (68M10) Internet topics (68M11) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12)

Cited In (31)

• A formal theory of choreographic programming
• Connecting open systems of communicating finite state machines
• Enforcing availability in failure-aware communicating systems
• Global types with internal delegation
• Title not available (Why is that?)
• Globally Governed Session Semantics
• Parameterised Multiparty Session Types
• Title not available (Why is that?)
• Realisability of global models of interaction
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Global protocol implementations via attribute-based communication
• Exploring type-level bisimilarity towards more expressive multiparty session types
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• Automata for analysing service contracts
• Title not available (Why is that?)
• A type checking algorithm for concurrent object protocols
• Concurrent reversible sessions
• The evolution of Jolie. From orchestrations to adaptable choreographies
• Globally governed session semantics
• A gentle introduction to multiparty asynchronous session types
• Verifiable abstractions for contract-oriented systems
• Precise Subtyping for Asynchronous Multiparty Sessions
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Lightening global types
• Role-based development of dynamically evolving esembles
• Multiparty session types as coherence proofs
• A calculus of global interaction based on session types
• Complete multiparty session type projection with automata
• Discretionary Information Flow Control for Interaction-Oriented Specifications

Uses Software

• Casper

This page was built for publication: On global types and multi-party sessions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881091)