The operational behavior of control operators has been studied comprehensively in the past few decades, but type systems of control operators have not. There are distinct type systems for shift, control, and shift0 without any relationship between them, and there has not been a type system that directly corresponds to control0. This paper remedies this situation by giving a uniform type system for all the four control operators. Following Danvy and Filinski's approach, we derive a monomorphic type system from the CPS interpreter that defines the operational semantics of the four control operators. By implementing the typed CPS interpreter in Agda, we show that the CPS translation preserves types and that the calculus with all the four control operators is terminating. Furthermore, we show the relationship between our type system and the previous type systems for shift, control, and shift0.

翻译：过去几十年来，控制算子的操作行为已得到广泛研究，但其类型系统却鲜有涉及。目前shift、control和shift0算子各自拥有互不关联的类型系统，且尚未存在与control0算子直接对应的类型系统。本文通过为全部四种控制算子建立统一的类型系统弥补了这一空白。遵循Danvy与Filinski的研究方法，我们从定义四种控制算子操作语义的CPS解释器出发，推导出单态类型系统。通过在Agda中实现带类型的CPS解释器，证明了CPS转换具有类型保持性，且包含全部四种控制算子的演算系统具有终止性。此外，我们进一步阐明了所提类型系统与先前shift、control及shift0类型系统之间的关联。