Continuation passing style for effect handlers

Daniel Hillerström, Sam Lindley, Robert Atkey, K. C. Sivaramakrishnan

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

11 Citations (Scopus)

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
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
ISBN (Electronic)9783959770477
DOIs
Publication statusPublished - 30 Aug 2017
Event2nd International Conference on Formal Structures for Computation and Deduction 2017 - Oxford, United Kingdom
Duration: 3 Sep 20179 Sep 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume84
ISSN (Electronic)1868-8969

Conference

Conference2nd International Conference on Formal Structures for Computation and Deduction 2017
Abbreviated titleFSCD 2017
CountryUnited Kingdom
CityOxford
Period3/09/179/09/17

Keywords

  • Continuation passing style
  • Delimited control
  • Effect handlers

ASJC Scopus subject areas

  • Software

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

Cite this