CoqExtraction/LetouzeyOverview/5

5 Some signicant Coq developments using extraction

A list of user contributions related to extraction can be found at http://coq. inria.fr/contribs/extraction-eng.html. Let us highlight some of them, and also mention some developments not (yet?) in this list.

  • CoRN: This development done in Nijmegen contains in particular a constructive proof of the fundamental theorem of algebra. But all attempts made in order to compute approximations of polynomial roots by extraction have been unsuccessful up to now 2. This example illustrates how a large, stratied, mathematically-oriented development with a peculiar notion of logical/informative distinction can lead to a nightmare in term of extracted code eciency and readability.

  • Tait: This proof of strong normalization of simply typed λ-calculus produces after extraction a term interpretor 1. This study with H. Schwichtenberg et alii has allowed us to compare several proof assistants and their respective extractions. In particular Minlog turned out to allow a finer control of what was eliminated or kept during extraction, while Coq Prop/Set distinction was rather rigid. At the same time, Coq features concerning proof management were quite helpful, and the extracted code was decent, even if not as nice as the one obtained via Minlog.

  • FSets: Started with J.C. Filliâtre some years ago 3, this certification of Ocaml finite set and map libraries is now included in the Coq Standard Library. This example has allowed us to investigate a surprisingly wide range of questions, in particular concerning specications and implementations via Coq modules, or concerning the best style for expressing delicate algorithms (tactics or Fixpoint or Russell or Function). It has been one of the rst large example to benet from extraction of modules and functors.

  • CompCert: X. Leroy and alii have certied in Coq a compiler from C (with minor restrictions) to powerpc assembly 6. While this development is quite impressive, its extraction is rather straightforward, since Coq functions have been written in a direct, structural way. The compiler obtained by extraction is performing quite well.

  • Fingertrees: In 10, M. Sozeau experiments with his Russell framework. The ngertrees structure, relying heavily on dependent types, is a good testcase for both this framework and the extraction. In particular, the code obtained by extraction contains several unsafe type casts, its aspect could be improved but at least it can be executed and is reasonably eficient.