Verified Extraction from Coq to OCaml
summary
A verified extraction pipeline implemented in Coq proves that programs over first‑order inductive data types extracted from Coq safely interoperate with OCaml and cannot segfault, while higher‑order interoperation can be unsafe. The work formalizes MALfunction’s operational semantics, proves compiler correctness from erased Coq terms to MALfunction, and establishes a separate compilation theorem via step‑indexed realizability for first‑order types. A plugin emits MLF files, supports readback of inductive values, and benchmarks show optimized extracted code (through MALfunction into OCaml) performs like unverified extraction; built on MetaCoq.
AI-written summary · about
chapters (10)
- 0:00Verified extraction intro
- 1:27Motivation for verification
- 3:58Interoperability theorem
- 5:45Realizability semantics
- 9:59Pipeline to OCaml
- 12:30Compiler correctness
- 13:57Plugin implementation
- 16:23Benchmarking performance
- 17:28Future work
- 18:33Question and answer session
related talks
24mCode Extraction from Coq to ML-like languages
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
19mImplementing OCaml APIs in Coq
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
42mMetaCoq as a tool to prevent future unsoundness in Coq
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
01h 06mVerifying a compiler through equational means
23mVellvm: Formalizing the Informal