A logical account of subtyping for session types

Ross Horne; Luca Padovani

doi:10.1016/j.jlamp.2024.100986

A logical account of subtyping for session types

Ross Horne, Luca Padovani

Research output: Contribution to journal › Article › peer-review

20 Downloads (Pure)

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.

Original language	English
Article number	100986
Number of pages	20
Journal	Journal of Logical and Algebraic Methods in Programming
Volume	141
Early online date	28 May 2024
DOIs	https://doi.org/10.1016/j.jlamp.2024.100986
Publication status	Published - 1 Oct 2024

Keywords

session types
subtyping
linear logic
fixed points
termination

Access to Document

10.1016/j.jlamp.2024.100986Licence: CC BY 4.0

Horne-Padovani-JLAMP-2024-A-logical-account-of-subtyping-for-session-typesFinal published version, 778 KBLicence: CC BY 4.0

Cite this

@article{1733140c7a2a440b92afd9ec375073ec,

title = "A logical account of subtyping for session types",

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.",

keywords = "session types, subtyping, linear logic, fixed points, termination",

author = "Ross Horne and Luca Padovani",

note = "Previously published in the Proceedings 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, https://doi.org/10.4204/EPTCS.378.3",

year = "2024",

month = oct,

day = "1",

doi = "10.1016/j.jlamp.2024.100986",

language = "English",

volume = "141",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "2352-2208",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - A logical account of subtyping for session types

AU - Horne, Ross

AU - Padovani, Luca

N1 - Previously published in the Proceedings 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, https://doi.org/10.4204/EPTCS.378.3

PY - 2024/10/1

Y1 - 2024/10/1

N2 - 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.

AB - 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.

KW - session types

KW - subtyping

KW - linear logic

KW - fixed points

KW - termination

UR - https://doi.org/10.48550/arXiv.2304.06398

U2 - 10.1016/j.jlamp.2024.100986

DO - 10.1016/j.jlamp.2024.100986

M3 - Article

SN - 2352-2208

VL - 141

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

M1 - 100986

ER -

A logical account of subtyping for session types

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

A logical account of subtyping for session types

Cite this