===== Research =====

==== Summary of Works ====

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

<well>
**2019-today**
  * Some **automata** theory in Coq (upcoming)

**2019-today**
  * **NatDed**: a Coq encoding of 1st-order Predicate Calculus (using a Natural Deduction style). [[https://gitlab.math.univ-paris-diderot.fr/letouzey/natded|development page]], [[https://www.irif.fr/_media/rencontres/pps2019/letouzey.pdf|talk]] (at [[https://www.irif.fr/rencontres/pps2019/index|Journées PPS 2019]]).

**2016-today**
  * **MMaps** : a Coq library for modular finite maps (a.k.a. FMaps 2.0). [[https://github.com/coq-community/coq-mmaps|development page]].

**2015-2018**
  * Investigation of **Hofstadter's G** function and tree and mirror. [[https://www.irif.fr/~letouzey/hofstadter_g|development page]], [[https://hal.inria.fr/hal-01195587/document|tech report]], [[https://www.irif.fr/_media/rencontres/pps2018/letouzey.pdf|talk]] (at [[https://www.irif.fr/rencontres/pps2018/index|Journées PPS 2018]]).

**2000-2018**
  * Participation to the Coq development team. Maintenance and improvement of various subsystems (including extraction). A few highlights : [[https://github.com/coq/coq/blame/master/theories/Init/Nat.v|Nat]] (e.g. sqrt and log2) [[https://github.com/coq/coq/blame/master/theories/PArith/BinPosDef.v|BinPosDef]] (and similar N, Z files) [[https://github.com/coq/coq/blame/master/theories/MSets/MSetAVL.v|MSetAVL]] [[https://github.com/coq/coq/blame/master/theories/Numbers/NaryFunctions.v|NaryFunctions]]... [[https://github.com/coq/coq/commits/master?author=letouzey|Full commit list]].

**2008**
  * Coq Extraction, An overview. CiE2008. [[https://www.irif.fr/~letouzey/download/letouzey_extr_cie08.pdf|pdf]], [[https://www.irif.fr/~letouzey/bib8.txt|bib]].

**2006**
  * Coq, with Laurent Théry and Georges Gonthier. In "The Seventeen Provers of the World", Freek Wiedijk (Ed.), LNCS 3600, 2006. [[https://www.irif.fr/~letouzey/download/coq17provers.pdf|pdf]], [[https://www.irif.fr/~letouzey/bib7.txt|bib]].

**2005**
  * Implicit and noncomputational arguments using monads, with Bas Spitters. Technical report. [[https://www.irif.fr/~letouzey/download/Letouzey_Spitters_05.pdf|pdf]].
  * Program extraction from normalization proofs, with Ulrich Berger and Stefan Berghofer and Helmut Schwichtenberg. Invited article in journal "Studia Logica" 82, 2006. [[http://www.mathematik.uni-muenchen.de/~schwicht/papers/snextr05/snextr05.pdf|pdf]], [[https://www.irif.fr/~letouzey/bib6.txt|bib]].
  * A Large-Scale Experiment in Executing Extracted Programs, with Luís Cruz-Filipe, Calculemus'05. [[https://www.irif.fr/~letouzey/download/lcf_pl_extr05.pdf| pdf]], [[https://www.irif.fr/~letouzey/bib5.txt|bib]].

**2004**
  * Programmation fonctionnelle certifiée: **l'extraction de programmes** dans l'assistant Coq. **PhD thesis**. [[https://www.irif.fr/~letouzey/download/these_letouzey.pdf|official French pdf]], [[https://www.irif.fr/~letouzey/download/these_letouzey_English.pdf|English pdf]], [[https://www.irif.fr/~letouzey/bib4.txt|bib]].
  * Functors for Proofs and Programs, with Jean-Christophe Filliâtre, ESOP'04. [[https://hal.archives-ouvertes.fr/hal-00150913/document|pdf]], [[https://www.irif.fr/~letouzey/bib3.txt|bib]].

**2002**
  * A New Extraction for Coq, TYPES'02. [[https://hal.archives-ouvertes.fr/hal-00150914/document|pdf]], [[https://www.irif.fr/~letouzey/bib2.txt|bib]].

**2000**
  * Formalizing Stålmarck's Algorithm in Coq, with Laurent Théry, TPHOLs'00. [[https://hal.archives-ouvertes.fr/hal-00150915/document|pdf]], [[https://www.irif.fr/~letouzey/bib.txt|bib]].

</well>

==== 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
[[http://www.cs.swan.ac.uk/cie08/|"Computability in Europe"]] (CiE'08). [[https://www.irif.fr/~letouzey/download/letouzey_extr_cie08.pdf|pdf]], [[https://www.irif.fr/~letouzey/bib8.txt|bib]].

The corresponding [[https://www.irif.fr/~letouzey/download/examples_CiE2008.v|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: [[http://www.cs.ru.nl/~freek/comparison/index.html|Freek's page]], the one of [[http://www.informatik.uni-trier.de/~ley/db/conf/tphol/lncs3600.html|DBLP]], and a [[https://www.irif.fr/~letouzey/download/coq17provers.pdf|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
[[https://www.irif.fr/~letouzey/download/tait.tgz|here]].

This work is described in an invited
[[http://www.mathematik.uni-muenchen.de/~schwicht/papers/snextr05/snextr05.pdf|article]] for the special issue 82 of the Journal
[[http://www.studialogica.org/|Studia Logica]]. A [[https://www.irif.fr/~letouzey/bib6.txt|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 [[https://www.irif.fr/~letouzey/download/Letouzey_Spitters_05.pdf|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
[[http://c-corn.cs.kun.nl|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 [[http://imps.mcmaster.ca/calculemus-2005/|Calculemus'05]].
A [[https://www.irif.fr/~letouzey/download/lcf_pl_extr05.pdf|draft]] of this article, and a [[https://www.irif.fr/~letouzey/bib5.txt|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 [[http://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.html|Set]] standard library of OCaml. An article about this work
was accepted at [[http://www.cis.ksu.edu/santos/esop2004/|ESOP'04]].

  * The [[https://hal.archives-ouvertes.fr/hal-00150913/document|pdf]] and [[http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz|postscript]] of this article and a [[https://www.irif.fr/~letouzey/bib3.txt|bibtex]] entry.
  * The source code and more details are available [[http://www.lri.fr/~filliatr/fsets/|here]].

==== A new extraction for Coq ====

This work was at first an PhD internship at
[[http://www.lri.fr|LRI]], with Christine Paulin as supervisor.
The original subject was: //Execution of Coq proof terms//.

  * The final [[https://www.irif.fr/~letouzey/download/rapport_dea.ps.gz|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 [[https://www.irif.fr/~letouzey/download/these_letouzey.ps.gz|postscript]] or [[https://www.irif.fr/~letouzey/download/these_letouzey.pdf|pdf]]. A [[https://www.irif.fr/~letouzey/bib4.txt|bibtex]] entry. An English translation is available [[https://www.irif.fr/~letouzey/download/these_letouzey_English.ps.gz|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 [[https://www.irif.fr/~letouzey/download/extraction2002-slides.dvi|slides]] of this presentation, best viewed with [[http://gallium.inria.fr/advi|Active-Dvi]].
  * The [[https://hal.archives-ouvertes.fr/hal-00150914/document|article]] accepted for publication in the post-workshop proceedings. A [[https://www.irif.fr/~letouzey/bib2.txt|bibtex]] entry.

==== Stålmarck's Algorithm in Coq ====

Master degree internship at [[http://www-sop.inria.fr|INRIA Sophia Antipolis]].

  * The [[https://www.irif.fr/~letouzey/stalmarck/rapport.ps.gz|report]] (French only).
  * The [[https://www.irif.fr/~letouzey/stalmarck/index.html|Coq sources]] of this first version and their chart (Mirror of this [[http://www-sop.inria.fr/croap/CFC/stalmarck|URL]]).
  * A new version of this work, thanks to [[http://www-sop.inria.fr/lemme/stalmarck/|Laurent Théry]]:
    * The [[https://www.irif.fr/~letouzey/download/stal-new.tar.gz|Coq sources]].
    * An on-line [[http://www-sop.inria.fr/cgi-bin/lemme/stalmarck/run|interface]] for playing with the extracted program.
    * The joint [[https://hal.archives-ouvertes.fr/hal-00150915/document|article]] describing this new implementation. A [[https://www.irif.fr/~letouzey/bib.txt|bibtex]] entry.
    * This [[https://hal.archives-ouvertes.fr/hal-00150915/document|article]] has been presented during the [[http://www.cse.ogi.edu/tphols2000|TPHOLs'2000]] conference at Portland, Oregon, in August 2000. [[https://www.irif.fr/~letouzey/pic/tphols.jpg|See]] who was there...

==== Old : a scholar work on dynamic systems ====

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

{{https://www.irif.fr/~letouzey/pic/iterati3.gif}}

  * In [[https://www.irif.fr/~letouzey/download/logistic.doc|doc]].
  * In [[https://www.irif.fr/~letouzey/download/logistic.pdf|pdf]] after a translation to LaTeX. Exercise: compare these two versions and guess why most scientists use LaTeX...
  * A few [[https://www.irif.fr/~letouzey/download/figures.zip|images]].
  * A short bibliography: [[https://www.irif.fr/~letouzey/download/biblio.doc|doc]] or [[https://www.irif.fr/~letouzey/download/biblio.pdf|pdf]].