Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Wed 26 Aug 2020 14:30 - 14:45 at ICFP NY 6 - New York 6 Chair(s): Sukyoung Ryu
Thu 27 Aug 2020 02:30 - 02:45 at ICFP Asia 6 - Asia 6 Chair(s): Sukyoung Ryu

Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper we aim to achieve abstraction without regret for effect handlers.

We present a language for effect handlers in capability-passing style and an implementation of this language as a translation to simply-typed lambda calculus in iterated continuation-passing style. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is very general and allows us to generate code in any language that supports first-class functions.

We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine our language with a more restrictive type system. We present a type-directed translation for the refined language that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.

Wed 26 Aug

Displayed time zone: Eastern Time (US & Canada) change

14:30 - 16:25
New York 6ICFP Program at ICFP NY 6
Chair(s): Sukyoung Ryu KAIST

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp Schuster University of Tübingen, Germany, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
DOI Media Attached
14:45
15m
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. Giarrusso BedRock Systems, Leo Stefanesco IRIF, University Paris Diderot & CNRS, Amin Timany Aarhus University, Lars Birkedal Aarhus University, Robbert Krebbers Delft University of Technology
DOI Media Attached
15:00
15m
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš Tejiščák University of St Andrews
DOI Media Attached
15:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di Wang Carnegie Mellon University, David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
15:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin Lubin University of Chicago, Nick Collins University of Chicago, Cyrus Omar University of Michigan, Ravi Chugh University of Chicago
DOI Media Attached
15:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András Kovács Eötvös Loránd University
DOI Pre-print Media Attached
16:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul Downen University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK, Richard A. Eisenberg Tweag I/O
DOI Media Attached
16:15
10m
Day closing
Conference closing
ICFP Program
Stephanie Weirich University of Pennsylvania

Thu 27 Aug

Displayed time zone: Eastern Time (US & Canada) change

02:30 - 04:25
Asia 6ICFP Program at ICFP Asia 6
Chair(s): Sukyoung Ryu KAIST

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp Schuster University of Tübingen, Germany, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
DOI Media Attached
02:45
15m
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. Giarrusso BedRock Systems, Leo Stefanesco IRIF, University Paris Diderot & CNRS, Amin Timany Aarhus University, Lars Birkedal Aarhus University, Robbert Krebbers Delft University of Technology
DOI Media Attached
03:00
15m
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš Tejiščák University of St Andrews
DOI Media Attached
03:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di Wang Carnegie Mellon University, David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
03:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin Lubin University of Chicago, Nick Collins University of Chicago, Cyrus Omar University of Michigan, Ravi Chugh University of Chicago
DOI Media Attached
03:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András Kovács Eötvös Loránd University
DOI Pre-print Media Attached
04:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul Downen University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK, Richard A. Eisenberg Tweag I/O
DOI Media Attached
04:15
10m
Day closing
Conference closing
ICFP Program
Stephanie Weirich University of Pennsylvania