Type System for Four Delimited Control Operators

Explore a 19-minute conference talk presented at ACM SIGPLAN's GPCE (Generative Programming: Concepts & Experiences) that delves into the development of a uniform type system for four delimited control operators. Learn how the researchers address the gap in type systems for control operators by deriving a monomorphic type system from a CPS (Continuation-Passing Style) interpreter. Discover the process of implementing the typed CPS interpreter in Agda to demonstrate type preservation and termination properties. Gain insights into the relationships between the newly proposed type system and previous type systems for shift, control, and shift0 operators. Understand the significance of this work in providing a comprehensive type system that directly corresponds to the control0 operator, which was previously lacking.

[GPCE] Type System for Four Delimited Control Operators