On Evaluation Contexts, Continuations, and the Rest of Computation

Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.

On Evaluation Contexts, Continuations, and the Rest of Computation

Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuations-as-evaluation-contexts are the defunctionalized representation of the continuation of a single-step reduction function and that continuations-as-the-rest-of-thecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the single-step reducer. The only difference is how these evaluation contexts are interpreted: a ‘plug’ interpretation yields one-step reduction, whereas a ‘refocus’ interpretation yields evaluation.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


I wonder if this result could have been achieved by appropriate instantiation of Milner's wide reactive systems (another instance being bigraphs)...