Session coalgebras: a coalgebraic view on session types and communication protocols

DOI10.1007/978-3-030-72019-3_14MaRDI QIDQ2233467zbMATH OpenOpenAlexFDO

Authors Alex C. Keizer, Henning Basold, Jorge A. Pérez

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

coalgebrasession typescoinductionprocess calculi

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Compositional methods are central to the development and verification of software systems. They allow to break down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that programs interact with channels according to a certain protocol, whether the intended messages are exchanged in a certain order. In this paper, we put on our coalgebraic spectacles to investigate session types, a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation makes it possible to elegantly derive a decidable type system with subtyping for $pi$-calculus processes, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective agree with the existing ones.

Recommendations

• scientific article; zbMATH DE number 7075898
• A calculus of global interaction based on session types
• Session types as intuitionistic linear propositions
• scientific article; zbMATH DE number 7559468
• A semantic deconstruction of session types
• Context-free session types for applied pi-calculus
• Fairness and communication-based semantics for session-typed languages
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus

Cites work

• scientific article; zbMATH DE number 2080757 (Why is no real title available?)
• scientific article; zbMATH DE number 1398002 (Why is no real title available?)
• A New Type System for Deadlock-Free Processes
• A calculus of mobile processes. I
• A lattice-theoretical fixpoint theorem and its applications
• A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday
• A theory of contracts for web services
• An intensionally fully-abstract sheaf model for \(\pi\)
• Behavioral polymorphism and parametricity in session-based communication
• Complete Lattices and Up-To Techniques
• Computer Aided Verification
• Context-free session types
• Deadlock and lock freedom in the linear \(\pi\)-calculus
• Fundamentals of session types
• Global progress for dynamically interleaved multiparty sessions
• Multiparty asynchronous session types
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• Multiparty session types meet communicating automata
• Polynomial functors and polynomial monads
• Session coalgebras: a coalgebraic view on session types and communication protocols
• Structured coalgebras and minimal HD-automata for the \(\pi\)-calculus
• Subtyping for session types in the pi calculus
• Talking bananas: structural recursion for session types
• The \(\pi\)-calculus: A theory of mobile processes
• The art of modelling computational systems: a journey from logic and concurrency to security and privacy. Essays dedicated to Catuscia Palamidessi on the occasion of her 60th birthday
• Typestate: A programming language concept for enhancing software reliability
• Using higher-order contracts to model session types

Cited in

(5)

• Session coalgebras: a coalgebraic view on session types and communication protocols
• The different shades of infinite session types
• Complete multiparty session type projection with automata
• System \(F^\mu_\omega\) with context-free session types
• scientific article; zbMATH DE number 6851955 (Why is no real title available?)

This page was built for publication: Session coalgebras: a coalgebraic view on session types and communication protocols

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