Typing, Representing, and Abstracting Control: Functional Pearl
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 Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change
10:20 - 10:45 Research paper | Typing, Representing, and Abstracting Control: Functional Pearl TyDe Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany DOI | ||
10:45 - 11:10 Research paper | Extensible Type-Directed Editing TyDe DOI | ||
11:10 - 11:35 Research paper | Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming TyDe Victor Cacciari MiraldoUtrecht University, Netherlands, Alejandro SerranoUtrecht University, Netherlands DOI | ||
11:35 - 12:00 Research paper | Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL TyDe DOI |