Verified Extraction from Coq to OCaml

Explore a groundbreaking 21-minute video presentation from PLDI 2024 on verified extraction from Coq to OCaml. Delve into the development of a novel extraction pipeline, implemented and verified in Coq itself, that addresses the trusted code base (TCB) concerns in the Coq proof assistant's extraction process. Learn about the challenges and solutions in providing clear correctness theorems and guarantees for safe interoperability between Coq and OCaml. Discover how this work builds upon the MetaCoq project and utilizes the semantics of OCaml's intermediate language. Gain insights into the important differences between Coq programs' operational semantics and their extraction, with a focus on interoperability guarantees for first-order and higher-order programs. Access the full article and supplementary archive for a comprehensive understanding of this significant advancement in verified compilation and functional programming.

[PLDI24] Verified Extraction from Coq to OCaml