Separating Sessions Smoothly

TL;DR

This paper presents HGV, a modular core calculus for session-typed functional programming that guarantees deadlock freedom and confluence, with a formal correspondence to a process calculus based on hypersequents and classical linear logic.

Contribution

It introduces hyper-environments in HGV, enabling type-preserving structural congruence and a formal operational correspondence with HCP, extending support to Girard's Mix rule.

Findings

HGV ensures deadlock freedom and confluence.

HGV and HCP translations preserve and reflect reduction.

Supports channel forwarding and exceptions via Mix rule.

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.