For some of them, a more detailed description can be found below.

The extraction mechanism of Coq allows one to transform Coq proofs and functions into functional programs. We illustrate the behavior of this tool by reviewing several variants of Coq definitions for Euclidean division, as well as some more advanced examples. We then continue with a more general description of this tool: key features, main examples, strengths, limitations and perspectives.

Article presented at Conference "Computability in Europe" (CiE'08). pdf, bib.

The corresponding Coq script.

With Laurent Théry and Georges Gonthier.

When Freek Wiedijk suggested the idea of a volume comparing the main different proof assistants, I contributed a Coq version of the proof used as test-suite, e.g. the irrationality of sqrt(2). In the Coq section of the final volume, my Coq proof appears betwen the ones by Laurent Théry and Georges Gonthier. Surprisingly, DBLP now seems to count this as a publication…

Pointers about The Seventeen Provers: Freek's page, the one of DBLP, and a direct access to the Coq section.

Joint work with Ulrich Berger and Stefan Berghofer and Helmut Schwichtenberg.

We have developed three formalizations of Tait's normalization proof for the simply typed lambda-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs, programs are machine-extracted that implement variants of the well-known N.B.E. (Normalization By Evaluation) algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting. The source files of the Coq development are available here.

This work is described in an invited article for the special issue 82 of the Journal Studia Logica. A bibtex entry.

Joint work with Bas Spitters.

We propose a light way of embedding in Coq the Minlog's non-computational quantifiers due to Ulrich Berger. We used Tait's normalization proof and the concatenation of vectors as case studies for the extraction of programs. With little effort one can eliminate noncomputational arguments from extracted programs. One thus obtains extracted code that is not only closer to the intended one, but also decreases both the running time and the memory usage dramatically. Finally we noticed that this embedding corresponds to a monadic view, and then study the connection between Harrop formulas, lax modal logic and the Coq type theory.

A technical report on this topic.

Joint work with Luis Cruz-Filipe.

In this work, we tried to apply the Coq extraction framework (see below) to the FTA formalization. FTA stands for “Fundamental Theorem of Algebra”, i.e. the existence of complex roots for any non-constant complex polynomials. This formalization has been performed in Nijmegen, and is now part of the broader C-CoRN project. The challenge is hence to obtain an effective root-search program out of this formalization using extraction. Up to now, this goal has been unsuccessful, but interesting intermediate results have been obtained.

An article about this work was accepted at Calculemus'05. A draft of this article, and a bibtex entry.

Joint work with Jean-Christophe Filliâtre.

This work is an application of Coq modules and extraction to certify the Set standard library of OCaml. An article about this work was accepted at ESOP'04.

• The pdf and postscript of this article and a bibtex entry.
• The source code and more details are available here.

This work was at first an PhD internship at LRI, with Christine Paulin as supervisor. The original subject was: Execution of Coq proof terms.

• The final report of this internship (French only).

I have then continued my researches on this subject during my PhD, always under the supervision of Christine Paulin. Theoretical aspects have been developed and an implementation has been realized.

• My final French PhD manuscript in postscript or pdf. A bibtex entry. An English translation is available here. English proofreader much welcome!

In the middle of my PhD, I presented intermediate results at the TYPES'02 workshop in Berg en Dal, near Nijmegen, Netherlands, in April 2002.

• The slides of this presentation, best viewed with Active-Dvi.
• The article accepted for publication in the post-workshop proceedings. A bibtex entry.

Master degree internship at INRIA Sophia Antipolis.

• The report (French only).
• The Coq sources of this first version and their chart (Mirror of this URL).
• A new version of this work, thanks to Laurent Théry:
  • The Coq sources.
  • An on-line interface for playing with the extracted program.
  • The joint article describing this new implementation. A bibtex entry.
  • This article has been presented during the TPHOLs'2000 conference at Portland, Oregon, in August 2000. See who was there…

A small study of the logistic map f(x)=rx(1-x). In French only…

• In doc.
• In pdf after a translation to LaTeX. Exercise: compare these two versions and guess why most scientists use LaTeX…
• A few images.
• A short bibliography: doc or pdf.