2026-07-21T20:02:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14413 2024-03-06T10:54:21Z ddc:004 open_access

Separating Sessions Smoothly Fowler, Simon Kokke, Wen Dardha, Ornela Lindley, Sam Morris, J. Garrett session types hypersequents linear lambda calculus 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 a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Simon Fowler and Wen Kokke and Ornela Dardha and Sam Lindley and J. Garrett Morris 2021 Is Part Of LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2021.36 urn:nbn:de:0030-drops-144138 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.36 eng https://creativecommons.org/licenses/by/4.0/legalcode