Hydra's Heads – Anton Podkopaev
summary
Claims machine-checked correctness proofs of compilation and memory models, using Coq to turn 30-page paper proofs into a program-checked development and roughly 40,000 lines of formalization; demonstrates a verified pipeline from language-level weak memory models to x86 and ARM semantics, and develops an intermediate memory model plus work on the promising semantics family; cites the 4‑color Coq proof as precedent and stresses which constructions, lemmas, and counterexamples actually required new definitions and major refactorings.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:29What is Coq
- 4:55Formal verification basics
- 11:18Programming language semantics
- 18:59Memory models basics
- 27:30Memory models state of the art
- 33:09Career in formal verification
- 36:24Memory models across languages
- 39:55Future challenges in research
- 46:40Conclusion and Q&A
related talks
15mExperimenting in a Sociotechnical System
42mPNSQC 2014 - Karen Johnson
22mOptimize Your C++ Development While Working From Home
48mHow microteams change the way we collaborate. Again.
57mRemote Pairing
48m(Remote) Pair programming
59mCode With Me – Behind the Scenes
32mWhat Will a Programmer's Workday Look Like in 10 Years?