Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules

Explore a groundbreaking approach to verified compositional compilation presented in this 20-minute video from POPL 2024. Delve into a novel method for verifying compilation of open modules in first-order languages supporting global memory and pointers, without relying on assumptions about compiler internals. Learn how the researchers utilize a Kripke relation with memory protection as a uniform and composable semantic interface for compiler passes. Discover how this approach achieves compositional correctness theorems for realistic optimizing compilers, directly relating native semantics of open modules. Understand the implications for end-to-end verification of modular programs and how this method supports essential compositionality and adequacy properties. Examine the application of this approach to CompCert's full compilation chain and its impact on reducing verification complexity for heterogeneous modules.

[POPL'24] Fully Composable and Adequate Verified Compilation with Direct Refinements betwe...