Lightening global types

DOI10.1016/J.JLAMP.2015.06.003zbMATH Open1337.68064arXiv1406.3483OpenAlexW2963801928MaRDI QIDQ492916FDOQ492916

Authors: Tzu-Chun Chen 

Publication date: 21 August 2015

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

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.

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

Recommendations

• Composition and decomposition of multiparty sessions
• On global types and multi-party sessions
• A calculus of global interaction based on session types
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Global progress for dynamically interleaved multiparty sessions

zbMATH Keywords

session typescommunication centred programmingglobal types

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Multiparty session types meet communicating automata
• Multiparty asynchronous session types
• Session types for access and information flow control
• Dynamic multirole session types
• Conversation types
• On global types and multi-party sessions
• Global Progress in Dynamically Interleaved Multiparty Sessions
• A theory of design-by-contract for distributed multiparty interactions
• The Conversation Calculus: A Model of Service-Oriented Computation
• Title not available (Why is that?)
• Specifying stateful asynchronous properties for distributed programs
• Nested protocols in session types
• Session-Based Communication Optimisation for Higher-Order Mobile Processes

Cited In (1)

• Multiparty Session Types Within a Canonical Binary Theory, and Beyond

This page was built for publication: Lightening global types

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