Simon Fowler ; Wen Kokke ; Ornela Dardha ; Sam Lindley ; J. Garrett Morris - Separating Sessions Smoothly

lmcs:9361 - Logical Methods in Computer Science, July 12, 2023, Volume 19, Issue 3 - https://doi.org/10.46298/lmcs-19(3:3)2023
Separating Sessions SmoothlyArticle

Authors: Simon Fowler ; Wen Kokke ; Ornela Dardha ; Sam Lindley ; J. Garrett Morris

    This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain an operational correspondence between HGV and HCP -- a process calculus based on hypersequents and in a propositions-as-types correspondence with classical linear logic (CLL). Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard's Mix rule, a crucial ingredient for channel forwarding and exceptions.

    https://doi.org/10.46298/lmcs-19(3:3)2023
    Source: arXiv.org:2105.08996
    Volume: Volume 19, Issue 3
    Published on: July 12, 2023
    Accepted on: April 13, 2023
    Submitted on: April 19, 2022
    Keywords: Computer Science - Programming Languages
    Licence: Attribution 4.0 International (CC BY 4.0)
    Funding:
      Source : OpenAIRE Graph
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233
    • CAREER: Extensibility in Theory and Practice; Funder: National Science Foundation; Code: 2044815
    • Effect Handler Oriented Programming; Funder: National Science Foundation; Code: MR/T043830/1
    • From Data Types to Session Types---A Basis for Concurrency and Distribution; Funder: UK Research and Innovation; Code: EP/K034413/1
    • Session Types for Reliable Distributed Systems (STARDUST); Funder: UK Research and Innovation; Code: EP/T014628/1
    • A programming language bridging theory and practice for scientific data curation; Funder: European Commission; Code: 682315

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    2 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 3396 times.
    This article's PDF has been downloaded 698 times.