Denotation-based Compositional Compiler Verification
summary
Proposes a denotational framework that represents each statement by three behavior sets (normal, error, divergence) enriched with traces and distinguishes finite vs infinite divergence, defines composition and loops via separate least/greatest fixed points, and proves a semantic vs syntactic linking equivalence for open modules. Introduces a gamma function that reduces complex state-refinement obligations to set inclusion, recovers algebraic compositional proofs, and is exercised on the CompCert front-end and optimizations like dead-code elimination and constant propagation on simple imperative prototypes.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:23Simulation-based proof challenges
- 3:10Key question and approach
- 6:19Extending semantics to calls
- 10:36Compiler correctness proof method
- 15:14Conclusion and applications
related talks
15mSemantics of Sets of Programs
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
20mFully Composable and Adequate Verified Compilation with Direct Refinements betwe...
15mMonadic Compiler Calculation (Functional Pearl)
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
01h 06mVerifying a compiler through equational means
25mComposing Secure Compilers
21mCompositional pre-processing for automated reasoning in dependent type theory