A Cost-Aware Logical Framework
summary
Presents calf, a full-spectrum dependent type theory that treats cost as an effect and enforces an internal noninterference property so I/O behavior cannot depend on cost, with an extensional lock (phase distinction) separating intensional cost from extensional behavior. Implements cost as a single step effect, gives a counting model, and mechanizes recurrence-relation and physicist-style amortized analyses in Agda. Case studies: tight closed bound for Euclid, amortized batched queues, sequential and parallel merge sort; artifacts available.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:19Dependent Type Theory for Program Verification
- 1:53A CostAware Framework
- 3:07Cost as a Property
- 5:20cathincap
- 7:38extensional phase
- 8:47phase distinction
- 11:13Defining algorithms
- 13:46Case studies
- 15:13Models
- 17:26Counting Model
- 19:04Conclusion
related talks
23mA Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
15mA Modular Cost Analysis for Probabilistic Programs
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
15mDenotational Recurrence Extraction for Amortized Analysis
11mLocal algebraic effect theories
29mLogical Relations for Effect Capabilities
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
15mHandling Bidirectional Control Flow