A logical account of subtyping for session types

Horne, Ross and Padovani, Luca (2024) A logical account of subtyping for session types. Journal of Logical and Algebraic Methods in Programming, 141. 100986. ISSN 2352-2216 (https://doi.org/10.1016/j.jlamp.2024.100986)

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

Abstract

We study iso-recursive and equi-recursive 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. Both subtyping relations admit 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. We observe that, because of the logical setting in which they arise, these subtyping relations preserve termination in addition to the usual safety properties of sessions.

ORCID iDs

Horne, Ross ORCID logoORCID: https://orcid.org/0000-0003-0162-1901 and Padovani, Luca;
CORE (COnnecting REpositories)