A unifying type-theory for higher-order (amortized) cost analysis
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 04, 2021
- Source ID
- 10.1145/3434308
Entities
People
- Deepak Garg
- Jan Hoffmann
- Marco Gaboardi
- Vineet Rajani
Organizations
- Boston University
- Carnegie Mellon University
- Defense Advanced Research Projects Agency
- Max Planck Institute for Software Systems
- National Science Foundation