Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Thu 27 Sep 2018 10:20 - 10:45 at New York Central - Types Chair(s): Richard A. Eisenberg

A well known technique to implement a programming language with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to implement a family of control operators shift_i and reset_i . This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n control operators for the entire program upfront. In contrast, we allow different parts of the program to live at different levels. It turns out that taking shift_0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. Guided by the types, the translation applies well known techniques to avoiding administrative beta- and eta-redexes at all levels of the CPS hierarchy.

Thu 27 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:20 - 12:00
TypesTyDe at New York Central
Chair(s): Richard A. Eisenberg Bryn Mawr College, USA
10:20
25m
Research paper
Typing, Representing, and Abstracting Control: Functional Pearl
TyDe
Philipp Schuster University of Tübingen, Germany, Jonathan Immanuel Brachthäuser University of Tübingen, Germany
DOI
10:45
25m
Research paper
Extensible Type-Directed Editing
TyDe
Joomy Korkut Wesleyan University, USA, David Thrane Christiansen Galois, USA
DOI
11:10
25m
Research paper
Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming
TyDe
Victor Cacciari Miraldo Utrecht University, Netherlands, Alejandro Serrano Utrecht University, Netherlands
DOI
11:35
25m
Research paper
Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL
TyDe
Ilya Yanok USI Lugano, Switzerland, Nate Nystrom USI Lugano, Switzerland
DOI