一句话：为经典逻辑的线性 L-演算建立对话 duploid 语义，并据此证明 Hasegawa-Thielecke 定理。
本文从 Curry-Howard 对应出发，研究带对合否定的经典逻辑，提出线性经典 L-演算这一极化效应演算。为同时容纳 call-by-value 与 call-by-name，直接风格指称语义中复合失去结合性。作者在非结合范畴上定义图态射伴随，提出非结合的 duploid 与对话 duploid 语义，分别对应线性 call-by-push-value 的效应伴随和线性 continuations 的对话手性。线性经典 L-演算可在任意对话 duploid 中解释，并构成语法对话 duploid。作为应用，作者用语义和语法方式证明 Hasegawa-Thielecke 定理：中心映射与可 thunk 映射在任意对话 duploid 中一致。
In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L -calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, we define a notion of adjunction between graph morphisms on non-associative categories, which we use to formulate polarized and non-associative notions of symmetric monoidal closed duploid and of dialogue duploid. We show that they provide a direct style counterpart to adjunction models: linear effect adjunctions for the (linear) call-by-push-value calculus and dialogue chiralities for linear continuations, respectively. In particular, we show that the syntax of the linear classical L -calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2502-13033,
title = {Classical Notions of Computation and the Hasegawa-Thielecke Theorem},
author = {Éléonore Mangel and Paul-André Melliès and Guillaume Munch-Maccagnoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776715}
}