Separating Sessions Smoothly
Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, J. Garrett Morris
TL;DR
This work introduces Hypersequent GV ($HGV$), a modular core calculus for functional programming with session types that uses hyper-environments to ensure type-preserving structural congruence, enabling a clean operational correspondence with Hypersequent CP ($HCP$). It establishes preservation, progress, and strong normalisation for $HGV$, and shows that well-typed GV configurations embed into $HGV$ configurations and that tree-structured $HGV$ configurations correspond to GV. The authors provide a bidirectional operational correspondence between $HGV$ and $HCP$ through translations, including a refinement to $HGV$-to-$HCP$ via $HGV^*$, and extend the framework with forest-structure extensions (TC-Mix), simplified forwarding, and exceptions (EGV). They also discuss structure-preserving embeddings between GV and $HGV$, and outline further extensions (forests, Mix, exceptions) that preserve deadlock freedom while enabling richer concurrency topologies and fault-handling semantics.
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.