Incremental Certified Programming
summary
Claims a formal framework that makes specifications monotone over partial programs by defining a completion refinement relation and a notion of completeness and proving monotonicity (incrementality) equals reasoning stability. Provides an IncRease prototype in the Rocq Prover using typeclasses, systematically derives reformulations for a fragment of predicates (including an equality reworking that flips directions and adds side conditions), proves a dead‑code elimination lemma for CompCert with one branch removed, and integrates with QuickChick and a Fiat‑style synthesis adaptation.
AI-written summary · about
chapters (9)
- 0:00Incremental certified programming
- 1:26Incremental development challenges
- 3:54Idealized incremental proof
- 6:41Equality breaks incrementality
- 8:46Cook R’s monetary approach
- 9:28Formal framework for incrementality
- 12:19Coq case study: dead code elimination
- 13:22Lessons learned and future work
- 13:44Q&A
related talks
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
28mGradual Verification: Assuring Software Incrementally
24mIncremental Computation: What Is the Essence? (Invited Contribution)
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
16mTermination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules
01h 05mVerifying Infinitely Many Programs at Once
11mMorello Cerise: proving secure encapsulation (work in progress)
19mPredictable Verification using Intrinsic Definitions