Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Mon 24 Sep 2018 15:23 - 15:46 at Stifel Theatre - Continuations and Effects Chair(s): Martin Elsman

Dependent types are a powerful tool for maintaining program invariants. To take advantage of this aspect in real-world programming, efforts have been put into enriching dependently typed languages with missing constructs, most notably, effects. This paper presents a language that has two practically interesting ingredients: dependent inductive types, and the delimited control constructs shift and reset. When integrating delimited control into a dependently typed language, however, two challenges arise. First, the dynamic nature of control operators, which is the source of their expressiveness, can break fundamental language properties such as logical consistency and subject reduction. Second, CPS translations, which we often use to define the semantics of control operators, do not scale straightforwardly to dependently typed languages. We solve the former issue by restricting dependency of types, and the latter using answer-type polymorphism of pure terms. The main contribution of this paper is to give a sound type system of our language, as well as a type-preserving CPS translation. We also discuss various extensions, which would make our language more like a full-spectrum proof assistant but pose non-trivial issues.

Mon 24 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:00 - 16:10
Continuations and EffectsResearch Papers at Stifel Theatre
Chair(s): Martin Elsman University of Copenhagen, Denmark
15:00
23m
Talk
Capturing the Future by Replaying the Past (Functional Pearl)
Research Papers
DOI
15:23
23m
Talk
Handling Delimited Continuations with Dependent Types
Research Papers
Youyou Cong Ochanomizu University, Japan, Kenichi Asai Ochanomizu University
DOI
15:46
23m
Talk
Versatile Event Correlation with Algebraic Effects
Research Papers
Oliver Bračevac TU Darmstadt, Nada Amin University of Cambridge, Guido Salvaneschi TU Darmstadt, Sebastian Erdweg Delft University of Technology, Netherlands, Patrick Eugster Purdue University, Mira Mezini TU Darmstadt
DOI