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

DOI10.1007/978-3-030-72019-3_14zbMATH Open1473.68114arXiv2011.05712OpenAlexW3151288834MaRDI QIDQ2233467FDOQ2233467

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

Publication date: 18 October 2021

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.

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

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
• scientific article
• Fairness and communication-based semantics for session-typed languages
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus

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)

Cites Work

• A lattice-theoretical fixpoint theorem and its applications
• A calculus of mobile processes. I
• A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday
• Multiparty session types meet communicating automata
• Multiparty asynchronous session types
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• Typestate: A programming language concept for enhancing software reliability
• Subtyping for session types in the pi calculus
• The \(\pi\)-calculus: A theory of mobile processes
• A theory of contracts for web services
• Global progress for dynamically interleaved multiparty sessions
• A New Type System for Deadlock-Free Processes
• Title not available (Why is that?)
• Computer Aided Verification
• Behavioral polymorphism and parametricity in session-based communication
• Title not available (Why is that?)
• Complete Lattices and Up-To Techniques
• Structured coalgebras and minimal HD-automata for the \(\pi\)-calculus
• Polynomial functors and polynomial monads
• Fundamentals of session types
• Deadlock and lock freedom in the linear \(\pi\)-calculus
• An intensionally fully-abstract sheaf model for \(\pi\)
• Using higher-order contracts to model session types
• Talking bananas: structural recursion for session types
• 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
• Context-free session types
• Session coalgebras: a coalgebraic view on session types and communication protocols

Cited In (5)

• The different shades of infinite session types
• Session coalgebras: a coalgebraic view on session types and communication protocols
• Title not available (Why is that?)
• Complete multiparty session type projection with automata
• System \(F^\mu_\omega\) with context-free session types

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)