Structured programming for structured proving

Verifying programs interactively is far from trivial. While a number of recent research projects have successfully verified significant code bases, interactive program verification is still considered prohibitively difficult and cumbersome.

In this talk, I will demonstrate several techniques that I have (co)developed over the last few years, that can simplify the burden on the interactive prover.

The starting point is the recognition that interactive proving is very similar to programming. Anybody who has ever seen a proof in Coq will be able to attest that we can have spaghetti proofs just like we can have spaghetti programs.

But this also means that we can beneficially import programming language ideas, such as dynamic dispatch or type parametricity, to the world of mathematics and verification. I have applied several such ideas to reasoning about concurrency, information flow, and pointer aliasing, to obtain concise, reusable and even automated formal proofs in Coq.