一句话：为依赖类型语言引入 shift/reset，限制类型依赖并用答案类型多态给出可靠类型系统与保类型 CPS 翻译。
本文关注在依赖类型语言中集成定界控制操作 shift 和 reset 时遇到的两个难题：控制算子的动态性可能破坏逻辑一致性与主体归约等基本性质，而常用于定义控制算子语义的 CPS 翻译也难以直接扩展到依赖类型。作者通过限制类型的依赖关系，并对纯项采用答案类型多态来解决这些问题。论文的主要贡献是给出该语言的一个可靠类型系统，以及一个保持类型的 CPS 翻译，从而在保留依赖归纳类型的同时支持定界延续。文章还讨论了若干可扩展方向，使语言更接近全谱证明助手，但这些扩展带来非平凡的挑战。
Dependent types are a powerful tool for maintaining program invariants. To take advantage of this aspect in real-world programming, efforts have been put into enriching dependently typed languages with missing constructs, most notably, effects. This paper presents a language that has two practically interesting ingredients: dependent inductive types, and the delimited control constructs shift and reset. When integrating delimited control into a dependently typed language, however, two challenges arise. First, the dynamic nature of control operators, which is the source of their expressiveness, can break fundamental language properties such as logical consistency and subject reduction. Second, CPS translations, which we often use to define the semantics of control operators, do not scale straightforwardly to dependently typed languages. We solve the former issue by restricting dependency of types, and the latter using answer-type polymorphism of pure terms. The main contribution of this paper is to give a sound type system of our language, as well as a type-preserving CPS translation. We also discuss various extensions, which would make our language more like a full-spectrum proof assistant but pose non-trivial issues.