一句话：提出 Hypersequent GV，用超环境保证会话类型结构同余的类型保持，并与 HCP 建立保持及反映归约的操作对应。
论文面向带会话类型的函数式编程核心演算，目标是同时获得无死锁、合流与强规范化，并保持结构同余的类型安全性。作者提出 Hypersequent GV（HGV），其核心是用超环境（类型环境的集合）管理会话通道，从而使结构同余可类型保持。基于超矢列，论文定义过程演算 HCP，并建立 HGV 与 HCP 之间经由经典线性逻辑的命题即类型对应。两个方向的翻译均保持且反映归约，给出操作对应。HGV 还平滑扩展到 Girard 的 Mix 规则，以支持通道转发与异常等特性，体现了模块化与可扩展性。
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.
@article{paperbot2207,
title = {Separating Sessions Smoothly},
author = {Simon Fowler and Wen Kokke and Ornela Dardha and Sam Lindley and J. Garrett Morris},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 3},
year = {2023},
doi = {10.46298/lmcs-19(3:3)2023}
}