[Université Paris Diderot, INRIA]

Pierre Letouzey

Research works

Summary of Publications

For each publication, a more detailed description can be found below.

2008

  • Coq Extraction, An overview. CiE2008. pdf, bib

2006

  • Coq, with Laurent Théry and Georges Gonthier. In "The Seventeen Provers of the World", Freek Wiedijk (Ed.), LNCS 3600, 2006. pdf, bib

2005

  • Implicit and noncomputational arguments using monads, with Bas Spitters. Technical report. pdf.
  • Program extraction from normalization proofs, with Ulrich Berger and Stefan Berghofer and Helmut Schwichtenberg. Invited article in journal "Studia Logica" 82, 2006. pdf, bib.
  • A Large-Scale Experiment in Executing Extracted Programs, with Luís Cruz-Filipe, Calculemus'05. pdf, bib.

2004

  • Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. PhD thesis. official French ps and pdf, English ps, bib.
  • Functors for Proofs and Programs, with Jean-Christophe Filliâtre, ESOP'04. ps, bib.

2002

  • A New Extraction for Coq, TYPES'02. ps, bib.

2000

  • Formalizing Stålmarck's Algorithm in Coq, with Laurent Théry, TPHOLs'00. ps, bib.

Coq Extraction, an Overview

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.

Coq entry in The Seventeen Provers of the World

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.

A multi-prover proof of strong normalization

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.

Embedding Minlog's non-computational quantifiers in Coq

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.

Extracting the FTA formalization

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.

Functors for Proofs and Programs

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 postscript of this article, and a bibtex entry.
  • The source code and more information are available here.

A new extraction for Coq

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, in 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 PhD manuscript in postscript or pdf. A bibtex entry. The original manuscript is in French, but an preliminary English translation is now available here. Concerning this translation, any proofreader would be much welcomed !

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.

  • The slides of this presentation, best viewed with Active-Dvi.
  • The article accepted for publication in the Post-Workshop Proceedings. A bibtex entry.

Stålmarck's Algorithm in Coq

Master degree internship at INRIA Sophia Antipolis.

Old : a scholar work on dynamic systems

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

[LogisticFunction]
  • In Word, or auto-extractable zip (45 Ko).
  • This work is now available in LaTeX format: ps or pdf.
    Exercise: compare the two versions (doc/tex) and wonder why most scientists use LaTeX...
  • A few images.
  • A short bibliography: doc, ps, pdf.