Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 15:00 - 16:00 at PEPM - Keynote 2 Chair(s): Torben Mogensen

Dependently typed programs often contain a lot of information that is useful only for type checking but useless for execution. Sometimes the amount of such information not only makes the program slower but it also worsens the time/space complexity of the program. However, we should not have to make a program asymptotically slower just by describing it more precisely.

In this talk, I will illustrate how this happens and where traditional approaches to (proof) erasure, such as proof universes or compile-time irrelevance fall short. I will show that by addressing erasure directly, we can remove (much of) this overhead, and I will describe an automatic way of discovering and removing it, while retaining the convenience of fully dependent pattern matching. Finally, I’ll sketch possible ways forward, such as integration with additional modalities/quantities or erasure polymorphism.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:00 - 16:00: Keynote 2PEPM at PEPM
Chair(s): Torben MogensenDIKU, University of Copenhagen

Live stream: https://www.youtube.com/watch?v=Ps_rUSG1yg0

15:00 - 16:00
Erasure In Dependently Typed Programming