A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
summary
Presents λ-amor, an affine type theory that adds a modal potential type plus a graded cost monad and refinements, and proves soundness with a Kripke step-indexed logical relation. Shows a surprising simulation: effects plus potentials simulate coeffects, achieved by a new monad encoding cost as input potential. Embeds both RAML (call-by-value amortized) and dlPCF (call-by-name coeffect) into λ-amor and obtains completeness for cost analysis of PCF programs.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:48Lambda-amor goals
- 3:12Amortized cost analysis basics
- 8:20Lambda-amor technical ingredients
- 13:44FIFO queue example
- 15:35Lambda-amor model and soundness
- 17:04RAML and dlPCF unifying embeddings
- 21:49Coeffects via effects and potentials
- 22:11Summary and conclusion
related talks
23mA Cost-Aware Logical Framework
15mDenotational Recurrence Extraction for Amortized Analysis
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
18mMulti Types and Reasonable Space
15mRaising Expectations: Automating Expected Cost Analysis with Types
20mSemantic foundations of potential-synthesis for expected amortised-cost analysis
12mA Unified View of Modalities in Type Systems
15mA Modular Cost Analysis for Probabilistic Programs