Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra

This video presents a research talk from POPL 2025 that introduces a novel three-dimensional refinement algebra framework for unifying compositional verification and certified compilation. Learn how researchers from Yale University and Shanghai Jiao Tong University address the challenge of verifying large-scale, heterogeneous systems through a compositional semantics approach that operates across program modules, abstraction levels, and system state components. The 20-minute presentation demonstrates how this framework, mechanized in the Coq proof assistant, can accommodate various verification techniques with multiple practical use cases. Explore how this approach could overcome limitations of current methods that rely on simple, specialized operational models that are difficult to interface with one another. The research includes available and reusable artifacts, with supplementary materials accessible through the provided links to the published article and project webpage.