Continuation passing style for effect handlers

Research output: ResearchConference contribution

  • Daniel Hillerström
  • Sam Lindley
  • Robert Atkey
  • KC Sivaramakrishnan
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 publication2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
EditorsDale Miller
Place of PublicationGermany
Pages18:1-18:19
Number of pages19
DOIs
StatePublished - 3 Sep 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume84

    Research areas

  • effect handlers, delimited control, continuation passing system, CPS, algebraic effects

View graph of relations