Denotational Recurrence Extraction for Amortized Analysis
summary
A language-to-language translation extracts recurrences from a credit-annotated source into a cost-bearing simply-typed lambda calculus, using an affine type system and a modality for credits. The method models credits as creation/subtraction in extracted costs, interprets recurrences denotationally in posets, and proves a bounding theorem. Binary counter shows amortized cost two for increment and set is linear, and the framework handles complex examples like splay trees via lambda_A → lambda_C extraction.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:27Formal Recurrence Extraction
- 2:58Operational Semantics
- 4:00Previous Work
- 5:16Recurrences
- 7:28Amortized Analysis
- 9:12LambdaA
- 11:00LambdaA Code
- 11:43Recurrence Extraction for LambdaA
- 12:28Recurrence Extraction for Binary Counter
- 13:29Bounding Theorem
- 14:08Summary
related talks
23mA Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
39mA Reusable Machine-Calculus for Automated Resource Analyses
23mA Cost-Aware Logical Framework
15mA Modular Cost Analysis for Probabilistic Programs
14mAdequacy for Algebraic Effects Revisited
20mSemantic foundations of potential-synthesis for expected amortised-cost analysis
22mA Dependent Language with Type-Safe Program Extraction
16mFrom Linearity to Borrowing