Log in

No account? Create an account





September 15th, 2019




The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes “under lambdas.” We prove that machine evaluation is equivalent to standard-order evaluation.Unlike traditional abstract machines, delimited control plays a significant role in the machine’s behavior. In particular, the machine replaces the manipulation of a heap using store-based effects with disciplined management of the evaluation stack using control-based effects. In short, state is replaced with control.To further articulate this observation, we present a simulation of call-by-need in a call-by-value language using delimited control operation

September 6th, 2019


A systematic approach to delimited control with multiple prompts

Paul Downen and Zena M. Ariola
University of Oregon

July 29th, 2019


Typing, Representing, and Abstracting Control

Philipp Schuster and Jonathan Immanuel Brachthäuser, University of Tübingen, Germany

Abstract A well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a family of control operators shifti and reseti. This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n-control operators for the entire program upfront, but we allow different parts of the program to live at different levels. It turns out that taking shift0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. The translation avoids administrative beta- and eta-redexes at all levels of the CPS hierarchy, by iterating well-known techniques for the non-iterated CPS translation

July 26th, 2019


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.

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.

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.

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.
Powered by LiveJournal.com