On global types and multi-party sessions

DOI10.2168/LMCS-8(1:24)2012MaRDI QIDQ2881091zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cited in

(31)

• Discretionary Information Flow Control for Interaction-Oriented Specifications
• 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
• scientific article; zbMATH DE number 7215288 (Why is no real title available?)
• Globally Governed Session Semantics
• Parameterised Multiparty Session Types
• scientific article; zbMATH DE number 7269254 (Why is no real title available?)
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Global protocol implementations via attribute-based communication
• Realisability of global models of interaction
• Exploring type-level bisimilarity towards more expressive multiparty session types
• Automata for analysing service contracts
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• A type checking algorithm for concurrent object protocols
• scientific article; zbMATH DE number 7453961 (Why is no real title available?)
• Concurrent reversible sessions
• The evolution of Jolie. From orchestrations to adaptable choreographies
• A gentle introduction to multiparty asynchronous session types
• Verifiable abstractions for contract-oriented systems
• Globally governed session semantics
• Precise Subtyping for Asynchronous Multiparty Sessions
• Lightening global types
• scientific article; zbMATH DE number 6703933 (Why is no real title available?)
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types
• scientific article; zbMATH DE number 7269246 (Why is no real title available?)
• 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

Describes a project that uses

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)