Extraction to OCaml from Coq: Operational Correctness Verified in Coq
One of the central claims of fame of the Coq proof assistant is extraction, i.e. the ability to obtain efficient programs in industrial programming languages such as OCaml from programs written in Coq’s expressive dependent type theory, used, amongst many others, in the CompCert project.
For executables obtained by extraction, the extraction process is part of the TCB, as are Coq’s elaboration and kernel, and the compiler used to compile the extracted code.
The MetaCoq project aims at decreasing the TCB of Coq’s kernel by re-implementing it in Coq itself and proving it correct w.r.t. a formalisation of Coq’s type theory in Coq.
We aim at taking one step further, namely removing the extraction process from the TCB as well. Our goal is to provide a verified drop-in replacement for Coq’s extraction process to OCaml. To be able to start with a trustworthy and economic specification, we extract to the intermediate language of the OCaml compiler as specified in the Malfunction project.
We report on our ongoing effort to verify the operational correctness of the obtained programs.
Thu 15 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
16:00 - 17:30
|Interpreting OCaml GADTs into Coq|
MLPre-print Media Attached File Attached
|Extraction to OCaml from Coq: Operational Correctness Verified in Coq|
Yannick Forster Inria, Matthieu Sozeau Inria, Pierre Giraud Inria, Team Gallinette, Pierre-Marie Pédrot INRIA, Nicolas Tabareau InriaFile Attached
|Verify, but test: extracting property-based tests from F* specifications|