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.
Type de document :
Pré-publication, Document de travail
Appeared in the author's PhD thesis (Chapter III) along with more details. See (and cite) Guillau.. 2011
Liste complète des métadonnées


https://hal.inria.fr/inria-00587597
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : jeudi 21 avril 2011 - 00:45:40
Dernière modification le : mardi 11 octobre 2016 - 13:58:09
Document(s) archivé(s) le : jeudi 8 novembre 2012 - 17:00:47

Fichier

lkpol_delimited.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00587597, version 1

Collections

PPS | USPC

Citation

Guillaume Munch-Maccagnoni. From delimited CPS to polarisation. Appeared in the author's PhD thesis (Chapter III) along with more details. See (and cite) Guillau.. 2011. <inria-00587597>

Partager

Métriques

Consultations de
la notice

176

Téléchargements du document

97