Continuation Passing Style for Effect Handlers

Daniel Hillerström, Sam Lindley, Robert Atkey, KC Sivaramakrishnan

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present Continuation Passing Style (CPS) translations for Plotkin and Pretnar’s effect handlers with Hillerström and Lindley’s row-typed fine-grain call-by-value calculus of effect handlers as the source language. CPS translations of handlers are interesting theoretically, to explain the semantics of handlers, and also offer a practical implementation technique that does not require special support in the target language’s runtime. We begin with a first-order CPS translation into untyped lambda calculus which manages a stack of continuations and handlers as a curried sequence of arguments. We then refine the initial CPS translation first by uncurrying it to yield a properly tail-recursive translation and second by making it higher-order in order to contract administrative redexes at translation time. We prove that the higher-order CPS translation simulates effect handler reduction. We have implemented the higher-order CPS translation as a JavaScript backend for the Links programming language.
Original languageEnglish
Title of host publicationThe Second International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
EditorsDale Miller
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages19
ISBN (Electronic)978-3-95977-047-7
Publication statusPublished - 9 Sep 2017
EventSecond International Conference on Formal Structures for Computation and Deduction - Oxford, United Kingdom
Duration: 3 Sep 20179 Sep 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISSN (Electronic)1868-8969


ConferenceSecond International Conference on Formal Structures for Computation and Deduction
Abbreviated titleFSCD 2017
Country/TerritoryUnited Kingdom
Internet address


Dive into the research topics of 'Continuation Passing Style for Effect Handlers'. Together they form a unique fingerprint.

Cite this