Log in

No account? Create an account


Typing Control Operators in the CPS Hierarchy

Typing Control Operators in the CPS Hierarchy

Previous Entry Share Next Entry

Typing Control Operators in the CPS Hierarchy

Małgorzata Biernacka University of Wrocław
Dariusz Biernacki University of Wrocław
Sergueı Lenglet University of Wrocław

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 shifti and reseti, 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.
Powered by LiveJournal.com