💾 Archived View for dcreager.net › papers › Fowler2023.gmi captured on 2023-11-14 at 08:28:40. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2023-07-22)
-=-=-=-=-=-=-
Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, J. Garrett Morris. “Separating Sessions Smoothly”.
Accepted to LMCS, extended journal version of CONCUR'21 paper
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.