Reference. The Duality of Computation under Focus
Cite
Cited by (4)
Classical Notions of Computation and the Hasegawa-Thielecke Theorem mangel-2026-classical
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).
A theory of effects and resources: adjunction models and polarised calculi curien-2016-a
Polarised Intermediate Representation of Lambda Calculus with Sums munchmaccagnoni-2015-polarised
Focalisation and Classical Realisability munchmaccagnoni-2009-focalisation
Cites 27 works (3 here)
With notes (3)
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
External (24)
- A call-by-name lambda-calculus machine (2007)
- Polarized and focalized linear and classical proofs (2005)
- C'est maintenant qu'on calcule, au cœur de la dualité (Mémoire d'habilitation) (2005)
- Call-by-value is dual to call-by-name (2003)
- Étude de la polarisation en logique (2002)
- Locus Solum: From the rules of logic to the logic of rules (2001)
- The duality of computation (2000)
- A new deconstructive logic: linear logic (1997)
- A Curry-Howard foundation for functional computation with control (1997)
- Polarisation des preuves classiques et renversement (1996)
- Séquents qu'on calcule (Thèse de Doctorat) (1995)
- Back to direct style (1994)
- Orthogonal higher-order rewriting systems are confluent (1993)
- Continuation Semantics or Expressing Implication by Negation (Technical Report) (1993)
- Logic Programming with Focusing Proofs in Linear Logic (1992)
- λμ-calculus: An algorithmic interpretation of classical natural deduction (1992)
- A computational analysis of Girard's translation and LC (1992)
- Explicit substitutions (1991)
- A new constructive logic: classic logic (1991)
- A formulae-as-type notion of control (1990)
- Lambda-calcul : types et modèles (1990)
- Proofs and Types (1989)
- Call-by-name, call-by-value and the λ-calculus (1975)
- The Mechanical Evaluation of Expressions (1964)