Reference. The Duality of Computation under Focus

Cite

Cite as @curien-2010-the (helia, typst) · \cite{curien-2010-the} (LaTeX)
BibTeX
bibtex · 1 line
@inbook{curien-2010-the, title={The Duality of Computation under Focus}, ISBN={9783642152405}, ISSN={1861-2288}, url={http://dx.doi.org/10.1007/978-3-642-15240-5_13}, DOI={10.1007/978-3-642-15240-5_13}, booktitle={Theoretical Computer Science}, publisher={Springer Berlin Heidelberg}, author={Curien, Pierre-Louis and Munch-Maccagnoni, Guillaume}, year={2010}, pages={165–181} }
hayagriva YAML (typst)
yaml · 17 lines
curien-2010-the:
  type: chapter
  title: The Duality of Computation under Focus
  author:
  - Curien, Pierre-Louis
  - Munch-Maccagnoni, Guillaume
  date: 2010
  page-range: 165-181
  url: http://dx.doi.org/10.1007/978-3-642-15240-5_13
  serial-number:
    doi: 10.1007/978-3-642-15240-5_13
    isbn: '9783642152405'
    issn: 1861-2288
  parent:
    type: book
    title: Theoretical Computer Science
    publisher: Springer Berlin Heidelberg
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).
PDF · DOI · arXiv · pldb

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

DOI · pldb

Polarised Intermediate Representation of Lambda Calculus with Sums munchmaccagnoni-2015-polarised

DOI

Focalisation and Classical Realisability munchmaccagnoni-2009-focalisation

DOI
Cites 27 works (3 here)
With notes (3)

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
External (24)
curien-2010-the reference entries/refs/curien-2010-the/curien-2010-the.hel