Semantic foundations of potential-synthesis for expected amortised-cost analysis
summary
Ongoing work builds a semantic stack that synthesises potential functions for randomized data structures and guarantees amortised-cost bounds correct by construction. It combines a first-order language with a probability monad, a quantitative weakest-precondition layer, and SMT-based constraint synthesis; lower layers are proven sound so different quantity DSLs can be swapped without redoing proofs. Prototype focuses on practical trade-offs (expressive cost grammars vs SMT tractability) and aims to reproduce Atlas-style tight bounds more robustly; development is early but the architecture validates.
AI-written summary · about
chapters (7)
- 0:00Potential-synthesis foundations
- 1:48Amortized cost analysis basics
- 5:45Automated amortized analysis
- 9:41Atlas system and data structures
- 13:14Layered analysis architecture
- 16:44Quantitative logic and cost layer
- 17:26Q&A
related talks
49mSemantic Foundations for Probabilistic Programming
19mPresynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
23mA Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
20mOptimal Program Synthesis via Abstract Interpretation
15mA Modular Cost Analysis for Probabilistic Programs
19mA Pure Demand Operational Semantics with Applications to Program Analysis
15mRaising Expectations: Automating Expected Cost Analysis with Types
30mSemantics-Guided Synthesis