一句话：用余代数给出会话类型的无语法语义，统一正则与上下文无关会话类型并导出可判定子类型系统。
该文研究会话类型这一行为类型系统，旨在为并发通信协议提供不依赖语法的语义基础，并统一处理正则与上下文无关会话类型。作者用余代数将基于会话的并发描述为状态，利用余归纳规范表示重新刻画类型等价、对偶与子类型；借助有理不动点建立会话余代数、有理不动点与会话类型的对应，并通过给会话余代数加栈来扩展到上下文无关情形。结果是在π演算上得到一个带子类型的可判定类型系统，且其关系与现有会话类型系统一致，同时揭示了通常语法式会话类型与无语法余代数方法之间的差异。
Compositional methods are central to the verification of software systems. 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 channels in a program interact following a certain protocol—whether messages are exchanged in the intended order. In this article, 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 enables us to derive a decidable type system with subtyping for the π-calculus, 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 coincide with existing ones. We further apply to session coalgebras the coalgebraic approach to regular languages via the so-called rational fixed point, inspired by the trinity of automata, regular languages, and regular expressions with session coalgebras, rational fixed point, and session types, respectively. We establish a suitable restriction on session coalgebras that determines a similar trinity, and reveals the mismatch between usual session types and our syntax-free coalgebraic approach. Furthermore, we extend our coalgebraic approach to account for context-free session types, by equipping session coalgebras with a stack.
@article{paperbot1608,
title = {Session Coalgebras: A Coalgebraic View on Regular and Context-free Session Types},
author = {Alex C. Keizer and Henning Basold and Jorge A. Pérez},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {3},
year = {2022},
doi = {10.1145/3527633}
}