An Operational Foundation for Delimited Continuations in the CPS Hierarchy

TL;DR

This paper introduces an abstract machine and reduction semantics for lambda-calculus with delimited continuations in the CPS hierarchy, enabling new applications like list prefix finding and normalization by evaluation.

Contribution

It provides a formal operational foundation for delimited continuations in the CPS hierarchy, including an abstract machine and semantics derived from CPS evaluators.

Findings

Developed an abstract machine from CPS evaluator

Constructed reduction semantics with explicit evaluation contexts

Demonstrated applications in list prefix finding and normalization

Abstract

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.