Separating Sessions Smoothly

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

doi:10.46298/lmcs-19(3:3)2023

Back

Journal article

Open access

Peer reviewed

Separating Sessions Smoothly

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley and J. Garrett Morris

Logical methods in computer science, Vol.19(3), pp.3:1-3:52

07/12/2023

DOI: 10.46298/lmcs-19(3:3)2023

Files and links (1)

url

https://doi.org/10.46298/lmcs-19(3:3)2023View

Published (Version of record) Open Access

Abstract

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.

Details

Title: Subtitle: Separating Sessions Smoothly
Creators: Simon Fowler
Wen Kokke
Ornela Dardha
Sam Lindley
J. Garrett Morris
Resource Type: Journal article
Publication Details: Logical methods in computer science, Vol.19(3), pp.3:1-3:52
DOI: 10.46298/lmcs-19(3:3)2023
ISSN: 1860-5974
eISSN: 1860-5974
Language: English
Date published: 07/12/2023
Academic Unit: Computer Science
Record Identifier: 9984445527502771

Metrics

5 Record Views