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

Displayed 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 Ahman University of Ljubljana, Matija Pretnar University of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40
10m
Talk
Dijkstra Monads Forever
POPL
Lucas Silver University of Pennsylvania, Steve Zdancewic University of Pennsylvania
Link to publication DOI
18:50
10m
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet Rajani MPI-SP, Marco Gaboardi Boston University, Deepak Garg Max Planck Institute for Software Systems, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
19:00
10m
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam Choudhury University of Pennsylvania, Harley D. Eades III Augusta University, Richard A. Eisenberg Tweag I/O, Stephanie Weirich University of Pennsylvania
Link to publication DOI Pre-print
19:10
10m
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron Moy Northeastern University, Phúc C. Nguyễn Google, Sam Tobin-Hochstadt Indiana University, David Van Horn University 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 Cockx TU Delft, Nicolas Tabareau Inria, Théo Winterhalter Inria — LS2N
Link to publication DOI Pre-print