Type System for Four Delimited Control OperatorsIn PersonBest Paper
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.
Tue 6 DecDisplayed time zone: Auckland, Wellington change
15:30 - 17:00 | |||
15:30 22mTalk | Language-Integrated Query for Temporal DataIn Person GPCE Simon Fowler University of Glasgow, Vashti Galpin University of Edinburgh, James Cheney University of Edinburgh DOI | ||
15:52 22mTalk | Type System for Four Delimited Control OperatorsIn PersonBest Paper GPCE DOI | ||
16:15 22mTalk | SQL to Stream with S2S: An Automatic Benchmark Generator for the Java Stream APIIn PersonTool Demo GPCE DOI | ||
16:37 8mOther | PC Chair's Report GPCE Yukiyoshi Kameyama University of Tsukuba |