Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols

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

*Bijbehorende auteur voor dit werk

OnderzoeksoutputAcademicpeer review

7 Citaten (Scopus)
47 Downloads (Pure)


Compositional methods are central to the development and verification of software systems. They allow breaking 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 휋-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.
Originele taal-2English
TitelProgramming Languages and Systems
Subtitel30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings
RedacteurenNobuko Yoshida
Plaats van productieCham
Aantal pagina's29
ISBN van elektronische versie978-3-030-72019-3
ISBN van geprinte versie978-3-030-72018-6
StatusPublished - 2021
EvenementEuropean Symposium on Programming -
Duur: 27-mrt.-20211-apr.-2021
Congresnummer: 30

Publicatie series

NaamLecture Notes in Computer Science
UitgeverijSpringer, Cham
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349


ConferenceEuropean Symposium on Programming
Verkorte titelESOP 2021

Citeer dit