Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 15-minute conference talk from OOPSLA 2025 that introduces a formal framework for incremental certified programming in proof assistants and dependently-typed programming languages. Learn how to address the fundamental challenge where proofs break during partial definitions and incremental changes because specifications aren't designed for intermediate incomplete program states. Discover the key concepts of completion refinement and completeness that enable systematic production of specifications valid at every development stage while preserving original statement intent. Examine the IncRease prototype implementation in the Rocq Prover, which leverages typeclasses for automation and extensibility while remaining independent of specific incompleteness handling mechanisms. Follow practical demonstrations through an incremental textbook formalization of the simply-typed λ-calculus and a complex case study involving incremental certified programming for CompCert's dead-code elimination optimization pass. Understand how this approach integrates with randomized property-based testing via QuickChick and combines with deductive synthesis using an incrementality-friendly adaptation of the Fiat library. Gain insights into the theoretical and practical foundations that enable systematic support for incremental certified programming, along with perspectives on future development challenges and opportunities.
