A logical account of subtyping for session types

Ross Horne, Luca Padovani

Research output: Contribution to journalArticlepeer-review

2 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 languageEnglish
Article number100986
Number of pages20
JournalJournal of Logical and Algebraic Methods in Programming
Volume141
Early online date28 May 2024
DOIs
Publication statusE-pub ahead of print - 28 May 2024

Keywords

  • session types
  • subtyping
  • linear logic
  • fixed points
  • termination

Fingerprint

Dive into the research topics of 'A logical account of subtyping for session types'. Together they form a unique fingerprint.
  • A logical account of subtyping for session types

    Horne, R. & Padovani, L., 13 Apr 2023, Proceedings 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. Castellani, I. & Scalas, A. (eds.). Waterloo, NSW: Open Publishing Association, Vol. 378. p. 26-37 12 p. (Electronic Proceedings in Theoretical Computer Science; vol. 378).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution book

    Open Access
    File
    1 Citation (Scopus)
    14 Downloads (Pure)

Cite this