Continuation passing style for effect handlers

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

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

11 Citations (Scopus)
20 Downloads (Pure)

Abstract

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
Publication statusPublished - 3 Sep 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume84

Keywords

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

Fingerprint Dive into the research topics of 'Continuation passing style for effect handlers'. Together they form a unique fingerprint.

Cite this