SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Tue 6 Dec 2022 15:52 - 16:15 at Seminar Room G135 - GPCE Session 1 Chair(s): Yukiyoshi Kameyama

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 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
GPCE Session 1GPCE at Seminar Room G135
Chair(s): Yukiyoshi Kameyama University of Tsukuba
15:30
22m
Talk
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
22m
Talk
Type System for Four Delimited Control OperatorsIn PersonBest Paper
GPCE
Chiaki Ishio Ochanomizu University, Kenichi Asai Ochanomizu University
DOI
16:15
22m
Talk
SQL to Stream with S2S: An Automatic Benchmark Generator for the Java Stream APIIn PersonTool Demo
GPCE
Filippo Schiavio USI Lugano, Andrea Rosà USI Lugano, Walter Binder USI Lugano
DOI
16:37
8m
Other
PC Chair's Report
GPCE
Yukiyoshi Kameyama University of Tsukuba