Certifying Complexity Analysis
summary
Plans to formalize the MWP imperative analysis in Coq, with an IMP-like language, MathComp matrices and a type system, and to prove the key soundness theorem: if a program is derivable with a matrix then all variable values have a polynomial bound. The analyzer uses MWP matrix closure plus addition and multiplication over a four-valued semi‑ring, is nondeterministic (multiple derivation paths), and succeeds if any path finishes; some paths or programs can fail, and constructive reformulation of the original proofs is a known challenge.
AI-written summary · about
chapters (10)
- 0:00Certifying complexity analysis
- 1:25Variable growth analysis
- 3:12MWP analysis technique
- 4:15Matrix dependency tracking
- 8:31Formalizing with proofs
- 12:48Certification process
- 13:51Motivation and goals
- 15:40Existential bounds matter
- 17:26Applications and use
- 19:54Q&A
related talks
31mAn Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
46mMechanizing Abstract Interpretation
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
14mVerification of Algorithm and Code Generation for Signal Transforms
28mWeighted programming: a programming paradigm for specifying mathematical models
42mMetaCoq as a tool to prevent future unsoundness in Coq
15mA Modular Cost Analysis for Probabilistic Programs
19mProgressful Interpreters for Efficient WebAssembly Mechanisation