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-2208 (https://doi.org/10.1016/j.jlamp.2024.100986)

Preview

Text. Filename: Horne-Padovani-JLAMP-2024-A-logical-account-of-subtyping-for-session-types.pdf Final Published Version License: 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.

• Share and Export
  

  RDF+XMLBibTeXRIOXX2 XMLRDF+N-TriplesJSONDublin CoreAtomSimple MetadataReferMETSHTML CitationASCII CitationOpenURL ContextObjectEndNoteOpenURL ContextObject in SpanMODSMPEG-21 DIDLEP3 XMLData Cite XMLRIS (EndNote Online, Zotero, Ref manager, etc)RDF+N3Multiline CSV
• Item metadata

  Item type:	Article
  ID code:	89417
  Dates:	Date Event 1 October 2024 Published 28 May 2024 Published Online 23 May 2024 Accepted
  Notes:	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
  Subjects:	Science > Mathematics > Electronic computers. Computer science Science > Mathematics
  Department:	Faculty of Science > Computer and Information Sciences
  Depositing user:	Pure Administrator
  Date deposited:	30 May 2024 14:27
  Last modified:	23 Jul 2024 01:33
  Related URLs:	Related item
  URI:	https://strathprints.strath.ac.uk/id/eprint/89417