一句话：提出 HCP，将线性逻辑扩展到超环境，从证明重写提取 LTS，并证明双相似、指称等价与带杠同余重合。
本文研究线性逻辑与 π 演算之间“证明即进程”对应在并行组合的语法与可观察语义上的不一致。作者提出 Hypersequent Classical Processes（HCP），受超序演算启发将线性逻辑保守扩展到超环境，即以环境集合为结构，并用 ⊗ 内化环境分离，使其对应并行进程行为。基于此，论文首次从证明重写中提取带标号迁移系统语义，并逻辑重构了 Merro 与 Sangiorgi 为 π 演算非阻塞 I/O 提出的延迟动作。作者还给出基于 Brzozowski 导数的指称语义，揭示 HCP 中的非干扰对应双重反导数的 Fubini 定理。评估方面，论文实例化双相似与带杠同余，证明双相似、指称等价与带杠同余三者重合，从而得到完全抽象结果。
We present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by ⊗ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini’s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.
@article{paperbot668,
title = {Better late than never: a fully-abstract semantics for classical processes},
author = {Wen Kokke and Fabrizio Montesi and Marco Peressotti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290337}
}