Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
summary
Formalizes a verified solver in Rocq that computes Taylor-series solutions for multivariate analytic ODE initial value problems following the Cauchy–Kovalevskaya construction, extracts coefficients algorithmically, and proves convergence with explicit truncation error bounds so the error is made arbitrarily small. Uses an abstract typeclass/setoid framework so the formalization is implementation‑agnostic, implements a faster interval arithmetic variant that outputs interval enclosures and plotting hooks, and ships artifacts demonstrating the method and its current performance limits.
AI-written summary · about
chapters (10)
- 0:00Solving ODEs in Rocq
- 2:06Computing solutions with guarantees
- 5:46Constructive reals and analytic ODEs
- 7:31Koshi-Kovalevski theorem
- 10:25Classical proof challenges
- 12:29Multivariate power series in Rocq
- 15:22Local solution algorithm
- 16:45Polynomial ODEs in Rocq
- 18:30Interval implementation and plotting
- 20:56Future work and efficiency
related talks
16mEnhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)
19mCertified Compilers à la Carte
15mThe HOL-Light library of Multivariate real analysis in Rocq
42mSession with the Rocq Development Team
23mTowards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
11mLocal algebraic effect theories
14mdxo: A System for Relational Algebra and Differentiation