We are happy to announce version 0.9.2 of the Coq Verified Extraction plugin for Coq 8.19, available as source and through Coq’s opam archive. This plugin builds on MetaCoq’s verified erasure and provides an alternative, verified extraction plugin to OCaml/malfunction. It produces untyped malfunction programs and typed interface files that can be further compiled using the malfunction/OCaml compiler to produce OCaml object files, linkable with regular OCaml programs. The proofs guarantee that the compilation of axiom-free, closed terms of firstorder inductive types (e.g. booleans or lists of natural numbers) evaluate to equivalent values in Coq or the compiled code. Definitions used to produce these objects have no typing restrictions, i.e. all of Coq’s constructs including ones not translatable to typeable OCaml terms can be used. In practice, the extraction procedure also accepts terms mentioning axioms, as long as those are implemented in OCaml, like the standard extraction system of Coq. The verified extraction supports all of Coq’s constructs including primitive and coinductive types, albeit the translation of coinductives and cofixpoints to lazy values, their encoding in OCaml, is not verified. The verified extraction that is run is a bootstrapped version, i.e. our verified extraction can extract itself.
The README.md file provides a detailed documentation of the available extraction commands.
See the tutorial for an introduction to the available commands. This version of verified extraction is complete enough to be used in real projects but is not quite polished. We are happy to receive any kind of feedback on Coq’s Zulip MetaCoq channel if you try to use this in your project.
The article Verified Extraction from Coq to OCaml describes this system in detail.
3 Likes