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

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication30th 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
EditorsNobuko Yoshida
Place of PublicationCham
PublisherSpringer
Pages375-403
Number of pages29
ISBN (Electronic)978-3-030-72019-3
ISBN (Print)978-3-030-72018-6
DOIs
Publication statusPublished - 2021
EventEuropean Symposium on Programming -
Duration: 27-Mar-20211-Apr-2021
Conference number: 30

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume12648
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceEuropean Symposium on Programming
Abbreviated titleESOP 2021
Period27/03/202101/04/2021

Cite this