Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Mon 4 Sep 2017 17:02 - 17:25 at L1 - Effects Chair(s): Ben Lippmeier

We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.

We present three calculi, one per abstraction, extending Levy's call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.

Mon 4 Sep

Displayed time zone: Belfast change

16:40 - 18:10
EffectsResearch Papers at L1
Chair(s): Ben Lippmeier Digital Asset / UNSW Australia
16:40
22m
Talk
Abstracting Definitional Interpreters
Research Papers
David Darais University of Maryland, USA, Nicholas Labich University of Maryland, USA, Phúc C. Nguyễn University of Maryland, USA, David Van Horn University of Maryland, USA
DOI
17:02
22m
Talk
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Research Papers
Yannick Forster Saarland University, Germany / University of Cambridge, UK, Ohad Kammar University of Oxford, UK, Sam Lindley University of Edinburgh, UK, Matija Pretnar University of Ljubljana, Slovenia
DOI
17:25
22m
Talk
Imperative Functional Programs That Explain Their Work
Research Papers
Wilmer Ricciotti University of Edinburgh, UK, Jan Stolarek University of Edinburgh, UK, Roly Perera University of Edinburgh, UK / University of Glasgow, UK, James Cheney University of Edinburgh, UK
DOI
17:47
22m
Talk
Effect-Driven QuickChecking of Compilers
Research Papers
Jan Midtgaard DTU, Denmark, Mathias Nygaard Justesen DTU, Denmark, Patrick Kasting DTU, Denmark, Flemming Nielson DTU, Denmark, Hanne Riis Nielson DTU, Denmark
DOI