Reference. Classical Notions of Computation and the Hasegawa-Thielecke Theorem

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

Cite

Cite as @mangel-2026-classical (helia, typst) · \cite{mangel-2026-classical} (LaTeX)
BibTeX
bibtex · 1 line
@article{mangel-2026-classical, title={Classical Notions of Computation and the Hasegawa-Thielecke Theorem}, volume={10}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3776715}, DOI={10.1145/3776715}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Mangel, Éléonore and Melliès, Paul-André and Munch-Maccagnoni, Guillaume}, year={2026}, month=Jan, pages={2112–2141} }
hayagriva YAML (typst)
yaml · 19 lines
mangel-2026-classical:
  type: article
  title: Classical Notions of Computation and the Hasegawa-Thielecke Theorem
  author:
  - Mangel, Éléonore
  - Melliès, Paul-André
  - Munch-Maccagnoni, Guillaume
  date: 2026-01
  page-range: 2112-2141
  url: http://dx.doi.org/10.1145/3776715
  serial-number:
    doi: 10.1145/3776715
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 10
Cited by (1)

Syntax and semantics of focalisation with relative monads and comonads mangel-2026-syntax

The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing effectful computation. On the semantics side, this corresponds to an axiomatic and polarised notion of model of computation stated in terms of adjunctions over non-associative categories. In this paper, we study the special and delicate cases of resource and effect modalities in a general intuitionistic and linear setting: an exponential comonad ! (refining □) and a strong monad ◊. The starting point of our contribution is noticing that the completeness for a polarised syntax for ! and ◊ with respect to (co)monads in linear call-by-push-value models can be achieved if we move to relative (co)monads: more precisely, comonads relative to ↓ (the positive shift functor) for ! and monads relative to ↑ (the negative shift functor) for ◊. These specialisations of the concept of relative (co)monad to call-by-push-value adjunctions recently appeared. Yet the syntax we present arose from proof-theoretic consideration, without the link with relative (co)monads being noticed at the time. Our first remark is thus that (co)monads relative to a call-by-push-value adjunction have been motivated previously from a proof-theoretic perspective in the context of focalisation, which also provides a meta-language for these concepts in an effectful setting. We carry out the study of these modalities from the axiomatic, non-associative point of view. We recall the notion of adjunction over non-associative categories, and establish correspondence results between this notion of adjunction and that of relative adjunction. This correspondence is then extended to linear-non-linear and strong versions of adjunctions as needed to model ! and ◊.
arXiv
Cites 71 works (8 here)
With notes (8)

A theory of effects and resources: adjunction models and polarised calculi curien-2016-a

DOI · pldb

Formulae-as-types for an involutive negation munchmaccagnoni-2014-formulae

DOI

Models of a Non-associative Composition munchmaccagnoni-2014-models

DOI

The Duality of Computation under Focus curien-2010-the

DOI · arXiv

Focalisation and Classical Realisability munchmaccagnoni-2009-focalisation

DOI

On the unity of duality zeilberger-2008-on

DOI

Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalue

DOI

Linear logic girard_linear_1987

The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI
External (63)
mangel-2026-classical reference entries/refs/mangel-2026-classical/mangel-2026-classical.hel