Typed Dynamic Control Operators for Delimited Continuations

Abstract. We study the dynamic control operators for delimited continuations, control and prompt. Based on recent developments on purely functional CPS translations for them, we introduce a polymorphically typed calculus for these control operators which allows answer-type modification. We show that our calculus enjoys type soundness and is compatible with the CPS translation. We also show that the typed dynamic control operators can macro-express the typed static ones (shift and reset), while the converse direction is not possible, which exhibits a sharp contrast with the type-free case.

• Type: Conference
• Year: 2008
• Where: FLOPS
• Authors: Yukiyoshi Kameyama, Takuo Yonezawa
• Keywords: Automated Reasoning, Cps Translation, Dynamic Control Operators, FLOPS 2008, Typed Dynamic Control