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

icfp-2018-papers
15:00 - 16:10: Research Papers - Continuations and Effects at Stifel Theatre
Chair(s): Martin ElsmanUniversity of Copenhagen, Denmark
icfp-2018-papers15:00 - 15:23
Talk
DOI
icfp-2018-papers15:23 - 15:46
Talk
Youyou CongOchanomizu University, Japan, Kenichi AsaiOchanomizu University
DOI
icfp-2018-papers15:46 - 16:10
Talk
Oliver BrańćevacTU Darmstadt, Nada AminUniversity of Cambridge, Guido SalvaneschiTU Darmstadt, Sebastian ErdwegDelft University of Technology, Netherlands, Patrick EugsterPurdue University, Mira MeziniTU Darmstadt
DOI