Unifying compositional verification and certified compilation with a three-dimensional(…)
summary
A concrete claim: a three-dimensional algebra of refinement composes module interfaces, abstraction levels, and state views so compiler correctness, linking theorems, and program-logic specs combine as refinement squares. The framework is mechanized in Coq and reuses a Comert-style certified compilation stack (Compcertoe), a separation-algebra framing, and a state transformation primitive to encapsulate mutable C memory; the paper builds a CP language with private vars and proves linked assembly+C pipeline behaviors (e.g. Hello World) preserved.
AI-written summary · about
chapters (8)
- 0:00Compositional verification intro
- 3:00Two-dimensional refinement
- 6:56FX signatures and composition
- 10:28Refinement squares
- 12:40State with special composition
- 14:34Certified compilation counter
- 17:24Future directions
- 18:07Q&A
related talks
25mUniversal Composability is Secure Compilation
01h 04mCoq's vibrant ecosystem for verification engineering
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
15mIncremental Certified Programming
21mMechanised Hypersafety Proofs about Structured Data
27mC4: verified transactional objects
47mHow to trust a verified program?
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic