From delimited CPS to polarisation

Abstract : The understanding of continuation-passing style (CPS) translations, an historical source of denotational semantics for programming languages, benefits from notions brought by linear logic, such as focalisation, polarities and the involutive negation. Here we aim to show how linear logic helps as well when continuations are delimited, i.e. return and can be composed, in the sense of Danvy and Filinski. First we provide a polarised calculus with delimited control (first-class delimited continuations) which is, at the level of computation, a variant of Girard's polarised classical logic LC. It contains variants of delimited control calculi which spawned as answers to the question "what order of evaluation can we consider with delimited control?". Thus our polarised calculus is one answer which is unifying to some degree. Subsequently we decompose the calculus through polarised linear logic. The only difference with non-delimited continuations is the use of specific exponentials, that account for the specific semantics of the target of delimited CPS translation, as well as annotations of type-and-effect systems. As a by-product, we obtain an explanation of CPS translations through a factoring, each step of which accounts for distinct phenomena of CPS translations. Although the factoring also holds for non-delimited CPS translations, it did not appear in its entirety before.
Document type :
Preprints, Working Papers, ...
Liste complète des métadonnées

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/inria-00587597
Contributor : Guillaume Munch-Maccagnoni <>
Submitted on : Thursday, April 21, 2011 - 12:45:40 AM
Last modification on : Friday, January 4, 2019 - 5:32:59 PM
Document(s) archivé(s) le : Thursday, November 8, 2012 - 5:00:47 PM

File

lkpol_delimited.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00587597, version 1

Collections

Citation

Guillaume Munch-Maccagnoni. From delimited CPS to polarisation. 2011. ⟨inria-00587597⟩

Share

Metrics

Record views

229

Files downloads

135