Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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, ...
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Guillaume Munch-Maccagnoni Connect in order to contact the contributor
Submitted on : Thursday, April 21, 2011 - 12:45:40 AM
Last modification on : Saturday, March 28, 2020 - 2:17:01 AM
Long-term archiving on: : Thursday, November 8, 2012 - 5:00:47 PM


Files produced by the author(s)


  • HAL Id : inria-00587597, version 1



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



Record views


Files downloads