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

This paper presents λ-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it. λ-amor introduces a new modal type for representing potentials – costs that have been accounted for, but not yet incurred, which are central to amortized analysis. Additionally, λ-amor relies on standard type-theoretic concepts like affineness, refinement types and an indexed cost monad. λ-amor is proved sound using a rather simple logical relation. We embed two existing type systems for cost analysis in λ-amor showing that, despite its simplicity, λ-amor can simulate cost analysis for different evaluation strategies (call-by-name and call-by-value), in different styles (effect-based and coeffect-based), and with or without amortization. One of the embeddings also implies that λ-amor is relatively complete for all terminating PCF programs.

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