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

Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop a novel version of such a graded dependent type system, including functions, tensor products, additive sums, and a unit type. Since standard operational semantics is resource-agnostic, we develop a heap-based operational semantics and prove a soundness theorem that shows correct usage of resources. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources and single pointer property for linear resources, can be derived from this theorem. We expect that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.

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
10m
Talk
Asynchronous Effects
POPL
Danel AhmanUniversity of Ljubljana, Matija PretnarUniversity of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40
10m
Talk
Dijkstra Monads Forever
POPL
Lucas SilverUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI
18:50
10m
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
10m
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
10m
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
10m
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