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

Some parts of dependently typed programs constitute evidence of their type-correctness and, once checked, are unnecessary for execution. These parts can easily become asymptotically larger than the remaining runtime-useful computation, which can cause normally linear-time programs run in exponential time, or worse. We should not make programs run slower by just describing them more precisely.

Current systems cannot erase such computation satisfactorily. By modelling erasure indirectly through type universes or irrelevance, they impose the limitations of these means to erasure. Some useless computation then cannot be erased and idiomatic programs remain asymptotically sub-optimal.

In this paper, we explain why we need erasure, that it is different from other concepts like irrelevance, and propose a dependently typed calculus with pattern matching with erasure annotations to model it. We show that erasure in well-typed programs is sound in that it commutes with reduction. Assuming the Church-Rosser property, erasure furthermore preserves convertibility in general.

We also give an erasure inference algorithm for erasure-unannotated or partially annotated programs and prove it sound, complete, and optimal with respect to the typing rules of the calculus.

Finally, we show that this erasure method is effective in that it can not only recover the expected asymptotic complexity in compiled programs at run time, but it can also shorten compilation times.

Wed 26 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

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

Public livestreams: YouTube, Bilibili (China)

14:30 - 14:45
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
DOI Media Attached
14:45 - 15:00
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft University of Technology
DOI Media Attached
15:00 - 15:15
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš TejiščákUniversity of St Andrews
DOI Media Attached
15:15 - 15:30
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI Media Attached
15:30 - 15:45
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI Media Attached
15:45 - 16:00
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print Media Attached
16:00 - 16:15
Talk
Kinds are Calling Conventions
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI Media Attached
16:15 - 16:25
Day closing
Conference closing
ICFP Program
Stephanie WeirichUniversity of Pennsylvania

Thu 27 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

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

Public livestreams: YouTube, Bilibili (China)

02:30 - 02:45
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
DOI Media Attached
02:45 - 03:00
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft University of Technology
DOI Media Attached
03:00 - 03:15
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš TejiščákUniversity of St Andrews
DOI Media Attached
03:15 - 03:30
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI Media Attached
03:30 - 03:45
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI Media Attached
03:45 - 04:00
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print Media Attached
04:00 - 04:15
Talk
Kinds are Calling Conventions
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI Media Attached
04:15 - 04:25
Day closing
Conference closing
ICFP Program
Stephanie WeirichUniversity of Pennsylvania