Towards verified extraction
Our commitment with formal verification implies a strong
concern about the verification of the Coq extraction
mechanism itself.
concern about the verification of the Coq extraction
mechanism itself.
The MetaCoq project aims to do exactly that, with horizon 2022 for having a first prototype.
The expected outcome is an extraction mechanism from Coq to OCaml, formally verified in Coq.
This will ensure the total verification of the OCaml code obtained by our team and used in real-world
applications. Our team actively supports the MetaCoq project for verification of extraction.
The expected outcome is an extraction mechanism from Coq to OCaml, formally verified in Coq.
This will ensure the total verification of the OCaml code obtained by our team and used in real-world
applications. Our team actively supports the MetaCoq project for verification of extraction.
While this goal is not reached, we have developed a method for extracting Coq code
to the OCaml in the safest way possible. The details can be found in the appendix of this article
to the OCaml in the safest way possible. The details can be found in the appendix of this article