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
  • From Data Types to Session Types---A Basis for Concurrency and Distribution; Funder: UK Research and Innovation; Code: EP/K034413/1
  • Effect Handler Oriented Programming; Funder: UK Research and Innovation; Code: MR/T043830/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
  • CAREER: Extensibility in Theory and Practice; Funder: National Science Foundation; Code: 2044815
  • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233

Classifications

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

3 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3697 times.
This article's PDF has been downloaded 761 times.