Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 19:10 - 19:20 at POPL-B - Types and Proof Assistance

Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks between the boundaries of typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the pragmatics of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead.

Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of the program.

We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead—most cases more than 2× overhead and up to 70× in the worst case—and reduce the overhead to 0 in most cases and 1.6× in the worst case.

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

18:30 - 19:30: Types and Proof AssistancePOPL at POPL-B
18:30 - 18:40
Talk
Asynchronous Effects
POPL
Danel AhmanUniversity of Ljubljana, Matija PretnarUniversity of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40 - 18:50
Talk
Dijkstra Monads Forever
POPL
Lucas SilverUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI
18:50 - 19:00
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet RajaniMPI-SP, Marco GaboardiBoston University, Deepak GargMax Planck Institute for Software Systems, Jan HoffmannCarnegie Mellon University
Link to publication DOI
19:00 - 19:10
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam ChoudhuryUniversity of Pennsylvania, Harley D. Eades IIIAugusta University, Richard A. EisenbergTweag I/O, Stephanie WeirichUniversity of Pennsylvania
Link to publication DOI Pre-print
19:10 - 19:20
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron MoyNortheastern University, Phúc C. NguyễnGoogle, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland, USA
Link to publication DOI Pre-print
19:20 - 19:30
Talk
The Taming of the Rew: A Type Theory with Computational Assumptions
POPL
Jesper CockxTU Delft, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Pre-print