A Functional Abstraction of Typed Invocation Contexts

TL;DR

This paper extends a functional approach to typed invocation contexts from shift/reset to control/prompt, capturing their dynamic behavior through a trail-based type system derived from CPS semantics.

Contribution

It generalizes the functional abstraction of typed contexts to control and prompt, incorporating trail representations to handle their dynamic context manipulation.

Findings

Derived a type system encoding CPS constraints for control and prompt

Showed how trail-based functional representation captures dynamic context behavior

Extended the semantic derivation from shift/reset to control/prompt

Abstract

In their paper "A Functional Abstraction of Typed Contexts", Danvy and Filinski show how to derive a monomorphic type system of the shift and reset operators from a CPS semantics. In this paper, we show how this method scales to Felleisen's control and prompt operators. Compared to shift and reset, control and prompt exhibit a more dynamic behavior, in that they can manipulate a trail of contexts surrounding the invocation of previously captured continuations. Our key observation is that, by adopting a functional representation of trails in the CPS semantics, we can derive a type system that encodes all and only constraints imposed by the CPS semantics.