Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Wednesday, November 13, 2013 - 11:14:06 AM
Last modification on : Saturday, November 21, 2020 - 9:54:03 AM
Long-term archiving on: : Friday, February 14, 2014 - 3:36:07 PM


Files produced by the author(s)



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. pp.149-160, ⟨10.1145/2003476.2003498⟩. ⟨hal-00903834⟩



Record views


Files downloads