A Functional Abstraction of Typed Trails

Felleisen's control and prompt are a pair of control operators that can dynamically change the extent of captured continuations. The behavior enables implementing non-trivial algorithms, but also complicates the semantics of programs. We present our preliminary work on designing a general type system for control/prompt. Following previous studies on typing control operators, we identify necessary typing constraints by carefully analyzing the CPS translation. As a result, we obtain a terminating type system that fully reflects how contexts compose and propagate at runtime.