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).

翻译：本着证明与程序之间的柯里-霍华德对应精神，我们利用极化效应演算——线性经典L演算，定义并研究了一种具有计算性对合否定的经典逻辑语法与语义。为该演算设计指称语义的主要挑战在于同时容纳按值调用与按名调用两种求值策略，这导致了复合运算结合律的失效。为解决此问题，我们在非结合范畴上定义了图态射间的伴随概念，并以此形式化极化与非结合的对称幺半闭双重复形及对话双重复形概念。我们证明它们为伴随模型提供了直接风格的对偶：分别对应（线性）按推送值调用演算的线性效应伴随，以及线性延续的对话手性。特别地，我们证明线性经典L演算的语法可在任意对话双重复形中解释，且其本身实际上定义了一个语法对话双重复形。作为应用，我们通过语义与语法两种方法建立了长谷川-蒂勒克定理，该定理表明在任意对话双重复形中（特别地，对于对称幺半范畴上的任意双重否定单子），中心映射与可延迟映射的概念是重合的。