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
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 .
Cites 71 works (8 here)
With notes (8)
A theory of effects and resources: adjunction models and polarised calculi curien-2016-a
Formulae-as-types for an involutive negation munchmaccagnoni-2014-formulae
Models of a Non-associative Composition munchmaccagnoni-2014-models
The Duality of Computation under Focus curien-2010-the
Focalisation and Classical Realisability munchmaccagnoni-2009-focalisation
On the unity of duality zeilberger-2008-on
Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalue
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.
External (63)
- Compiling with continuations, or without? whatever (2019)
- Duploid situations in concurrent games (2017)
- Contextual isomorphisms (2017)
- A micrological study of negation (2017)
- Note on Curry’s style for Linear Call-by-Push-Value (2017)
- Dialogue Categories and Chiralities (2016)
- The parametric continuation monad † (2015)
- The enriched effect calculus: syntax and semantics (2014)
- Freyd categories are Enriched Lawvere Theories (2014)
- Syntax and Models of a non-Associative Composition of Programs and Proofs (2013)
- Game Semantics in String Diagrams (2012)
- The diameter of associahedra (2012)
- Parametric monads and enriched adjunctions (2012)
- Intuitionistic Dual-intuitionistic Nets (2011)
- Resource modalities in tensor logic (2010)
- Focusing and polarization in linear, intuitionistic, and classical logics (2009)
- Categorical proof theory of classical propositional calculus (2006)
- Order-enriched categorical models of the classical sequent calculus (2006)
- Substructural simple type theories for separation and in-place update (2006)
- A Semantic Formulation of TT-Lifting and Logical Predicates for Computational Metalanguage (2005)
- Reducibility and ⊤⊤-lifting for computation types (2005)
- Asynchronous Games 3 An Innocent Model of Linear Logic (2005)
- On the call-by-value CPS transform and its semantics (2004)
- Sequentiality vs. concurrency in games and logic (2003)
- Adjunction Models For Call-By-Push-Value With Stacks (2003)
- Call-by-value is dual to call-by-name (2003)
- Completeness of continuation models for λμ-calculus (2002)
- Proof theory in the abstract (2002)
- Etude de la polarisation en logique (2002)
- Notions of Computation Determine Monads (2002)
- Premonoidal categories as categories with algebraic structure (2002)
- Axioms for Recursion in Call-by-Value (2001)
- Control categories and duality: on the categorical semantics of the lambda-mu calculus (2001)
- The duality of computation (2000)
- The structure of call-by-value (2000)
- Constructive Classical Logic as CPS-Calculus (2000)
- Classical logic and computation (2000)
- Direct Models for the Computational Lambda Calculus (1999)
- Call-by-Push-Value: A Subsuming Paradigm (1999)
- Classical logic, continuation semantics and abstract machines (1998)
- Weakly distributive categories (1997)
- A new deconstructive logic: linear logic (1997)
- Premonoidal categories and notions of computation (1997)
- Categorical Structure of Continuation Passing Style (1997)
- A symmetric lambda calculus for classical program extraction (1996)
- Linear logic, monads and the lambda calculus (1996)
- Polarisation des preuves classiques et renversement (1996)
- LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of the classical implication (1995)
- A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure (1995)
- Representing monads (1994)
- Axiomatic domain theory in categories of partial maps (1994)
- The Structure of Exponentials: Uncovering the Dynamics of Linear Logic Proofs (1993)
- Continuation Semantics or Expressing Implication by Negation (1993)
- A Game Semantics for Linear Logic (1992)
- A computational analysis of Girard's translation and LC (1992)
- Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction (1992)
- A new constructive logic: classic logic (1991)
- Notions of Computation and Monads (1991)
- An evaluation semantics for classical proofs (1991)
- A formulae-as-types notion of control (1990)
- Declarative Continuations and Categorical Duality (1989)
- Computational lambda-calculus and monads (1989)
- On Double Dualization Monads (1970)