一句话：通过 CPS 语义中调用迹的函数式表示，为 control/prompt 推导出恰好编码 CPS 约束的类型系统。
Danvy 与 Filinski 曾从 CPS 语义导出 shift/reset 的单态类型系统。本文将该方法推广到 Felleisen 的 control 与 prompt 算子。control/prompt 比 shift/reset 更具动态性，因为它们可以操纵围绕先前捕获的续延调用的一连串上下文（trail）。作者的关键观察是：在 CPS 语义中采用 trail 的函数式表示，就能推导出一个类型系统，使其恰好编码 CPS 语义所施加的全部约束。论文给出这一推导，并说明所得系统如何支持 control/prompt 的类型化。评估以理论推导及与 shift/reset 经典方法的对照为主，摘要未报告实现或实验。
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.
@article{paperbot1653,
title = {A Functional Abstraction of Typed Invocation Contexts},
author = {Youyou Cong and Chiaki Ishio and Kaho Honda and Kenichi Asai},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:34)2022}
}