A Dynamic Interpretation of the CPS Hierarchy

http://www.ii.uni.wroc.pl/~dabi/publications/APLAS12/materzok-biernacki-aplas12.pdf

A Dynamic Interpretation of the CPS Hierarchy

Marek Materzok and Dariusz Biernacki, University of Wrocław, Wrocław, Poland

Abstract: The CPS hierarchy of control operators shifti / reseti of Danvy and Filinski is a natural generalization of the shift and reset static control operators that allow for abstracting delimited control in a structured and CPS-guided manner. In this article we show that a dynamic variant of shift/reset, known as shift0 / reset0, where the discipline of static access to the stack of delimited continuations is relaxed, can fully express the CPS hierarchy. This result demonstrates the expressive power of shift0 / reset0 and it offers a new perspective on practical applications of the CPS hierarchy.

A Substructural Type Systemfor Delimited Continuations

http://homes.sice.indiana.edu/ccshan/binding/context.pdf

A Substructural Type System for Delimited Continuations

Oleg Kiselyov and Chung-chieh Shan

Abstract. We propose type systems that abstractly interpret small-step rather than big-step operational semantics. We treat an expression or evaluation context as a structure in a linear logic with hypothetical reasoning. Evaluation order is not only regulated by familiar focusing rules in the operational semantics, but also expressed by structural rules in the type system, so the types track control flow more closely. Binding and evaluation contexts are related, but the latter are linear. We use these ideas to build a type system for delimited continuations. It lets control operators change the answer type or act beyond the nearest dynamically-enclosing delimiter, yet needs no extra fields in judgments and arrow types to record answer types. The typing derivation of a direct-style program desugars it into continuation-passing style.

Typing Control Operators in the CPS Hierarchy

http://www.ii.uni.wroc.pl/~mabi/papers/biernacka-al-ppdp11.pdf

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.

An Operational Investigation of the CPS Hierarchy

https://link.springer.com/content/pdf/10.1007/3-540-49099-X_15.pdf

An Operational Investigation of the CPS Hierarchy

Olivier Danvy (University of Aarhus, Denmark) and Zhe Yang (New York University, USA)

Abstract.We explore the hierarchy of control induced by successive transformations into continuation-passing style (CPS) in the presence of "control delimiters" and "composable continuations". Specifically, we investigate the structural operational semantics associated with the CPS hierarchy. To this end, we characterize an operational notion of continuation semantics. We relate it to the traditional CPS transformation and we use it to account for the control operator shift and the control delimiter reset operationally. We then transcribe the resulting continuation semantics in ML, thus obtaining a native and modular implementation of the entire hierarchy. We illustrate it with several examples, the most significant of which is layered monads.