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

icfp-2017-papers
16:40 - 18:10: Research Papers - Effects at L1
Chair(s): Ben LippmeierDigital Asset / UNSW Australia
icfp-2017-papers150453600000016:40 - 17:02
Talk
David DaraisUniversity of Maryland, USA, Nicholas LabichUniversity of Maryland, USA, Phúc C. NguyễnUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA
DOI
icfp-2017-papers150453735000017:02 - 17:25
Talk
Yannick ForsterSaarland University, Germany / University of Cambridge, UK, Ohad KammarUniversity of Oxford, UK, Sam LindleyUniversity of Edinburgh, UK, Matija PretnarUniversity of Ljubljana, Slovenia
DOI
icfp-2017-papers150453870000017:25 - 17:47
Talk
Wilmer RicciottiUniversity of Edinburgh, UK, Jan StolarekUniversity of Edinburgh, UK, Roly PereraUniversity of Edinburgh, UK / University of Glasgow, UK, James CheneyUniversity of Edinburgh, UK
DOI
icfp-2017-papers150454005000017:47 - 18:10
Talk
Jan MidtgaardDTU, Denmark, Mathias Nygaard JustesenDTU, Denmark, Patrick KastingDTU, Denmark, Flemming NielsonDTU, Denmark, Hanne Riis NielsonDTU, Denmark
DOI