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 metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-00903834
Contributor : Sergueï Lenglet <>
Submitted on : Wednesday, November 13, 2013 - 11:14:06 AM
Last modification on : Friday, November 15, 2013 - 4:21:30 PM
Long-term archiving on : Friday, February 14, 2014 - 3:36:07 PM

File

hierarchy.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

145

Files downloads

291