Typing control operators in the CPS hierarchy

Abstract : The CPS hierarchy of Danvy and Filinski is a hierarchy of continuations that allows for expressing nested control effects characteristic of, e.g., non-deterministic programming or certain instances of normalization by evaluation. In this article, we present a comprehensive study of a typed version of the CPS hierarchy, where the typing discipline generalizes Danvy and Filinski's type system for control operators shift and reset. To this end, we define a typed family of control operators that give access to delimited continuations in the CPS hierarchy and that are slightly more flexible than Danvy and Filinski's family of control operators shift_i and reset_i, but, as we show, are equally expressive. For this type system, we prove subject reduction, soundness with respect to the CPS translation, and termination of evaluation. We also show that our results scale to a type system for even more flexible control operators expressible in the CPS hierarchy.
Type de document :
Communication dans un congrès
PPDP - Principles and Practice of Declarative Programming, Jul 2011, Odense, Denmark. ACM New York, pp.149-160, 2011, Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming. 〈10.1145/2003476.2003498〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00903834
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 13 novembre 2013 - 11:14:06
Dernière modification le : vendredi 15 novembre 2013 - 16:21:30
Document(s) archivé(s) le : vendredi 14 février 2014 - 15:36:07

Fichier

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

Identifiants

Citation

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet. Typing control operators in the CPS hierarchy. PPDP - Principles and Practice of Declarative Programming, Jul 2011, Odense, Denmark. ACM New York, pp.149-160, 2011, Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming. 〈10.1145/2003476.2003498〉. 〈hal-00903834〉

Partager

Métriques

Consultations de la notice

116

Téléchargements de fichiers

207