A logical account of subtyping for session types

Horne, Ross and Padovani, Luca; Castellani, Ilaria and Scalas, Alceste, eds. (2023) A logical account of subtyping for session types. In: Proceedings 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. Electronic Proceedings in Theoretical Computer Science, 378 . Open Publishing Association, Waterloo, NSW, pp. 26-37. (https://doi.org/10.4204/EPTCS.378.3)

[thumbnail of Horne-Padovani-EPTCS-2023-A-logical-account-of-subtyping-for-session-types]
Preview
 Text. Filename: Horne-Padovani-EPTCS-2023-A-logical-account-of-subtyping-for-session-types.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (174kB)| Preview

Abstract

We study the notion of subtyping for session types in a logical setting, where session types are propositions of multiplicative/additive linear logic extended with least and greatest fixed points. The resulting subtyping relation admits a simple characterization that can be roughly spelled out as the following lapalissade: every session type is larger than the smallest session type and smaller than the largest session type. At the same time, we observe that this subtyping, unlike traditional ones, preserves termination in addition to the usual safety properties of sessions. We present a calculus of sessions that adopts this subtyping relation and we show that subtyping, while useful in practice, is superfluous in the theory: every use of subtyping can be “compiled away” via a coercion semantics.

CORE (COnnecting REpositories)