Research works
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. 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 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 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.
This work was at first an PhD internship at LRI, with Christine Paulin as supervisor. The original subject was: Execution of Coq proof terms.
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.
In the middle of my PhD, I presented intermediate results at the TYPES'2002 workshop in Berg en Dal, near Nijmegen, Netherlands, in April 2002.
Master degree internship at INRIA Sophia Antipolis.
A small study of the logistic map f : x -> rx(1-x). In French only...