[Université Paris Diderot, INRIA]

Pierre Letouzey

Travaux de recherche

Liste des publications

Pour chaque publication, se trouve plus bas une description détaillée.

2008

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

2006

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

2005

  • Implicit and noncomputational arguments using monads, avec Bas Spitters. Rapport technique. pdf.
  • Program extraction from normalization proofs, avec Ulrich Berger, Stefan Berghofer et Helmut Schwichtenberg. Article invité dans la revue "Studia Logica" 82, 2006. pdf, bib.
  • A Large-Scale Experiment in Executing Extracted Programs, avec Luís Cruz-Filipe, Calculemus'05. pdf, bib.

2004

  • Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Thèse de doctorat. ps, pdf, bib.
  • Functors for Proofs and Programs, avec 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, avec Laurent Théry, TPHOLs'00. ps, bib.

Une vue d'ensemble de l'extraction Coq

Le mécanisme d'extraction de Coq permet de transformer des preuves Coq en programmes fonctionnels. Cet article a pour but d'illuster le comportement de cet outil sur plusieurs définitions possibles de la division euclidienne en Coq, ainsi que sur quelques exemples plus avancés. L'extraction est ensuite décrite de manière plus générale: propriétés-clés, principaux cas d'utilisation, forces, faiblesses et perspectives.

Article présenté à la conférence "Computability in Europe" (CiE'08). pdf, bib. Le script Coq correspondant.

Notice sur Coq pour Les Dix-Sept Prouveurs du Monde

Avec Laurent Théry et Georges Gonthier.

Lorsque Freek Wiedijk a lancé l'idée d'un recueil comparant les différents assistants de preuves majeurs, j'ai proposé une version Coq de la formalisation demandée, à savoir une preuve de l'irrationalité de la racine carré de 2. Étonnement, non seulement cette version a été retenue pour la section Coq de ce recueil (entouré par les propositions de Laurent Théry et Georges Gonthier), mais désormais DBLP compte cela comme une publication...

Quelques pointeurs concernant ce recueil: la page de Freek, celle de DBLP, et un lien direct vers la section coq du recueil.

Une preuve de normalisation forte multi-systèmes

Travail commun avec Ulrich Berger, Stefan Berghofer et Helmut Schwichtenberg.

Nous avons développé trois formalisations d'une preuve de normalisation à la Tait pour le lambda-calcul simplement typé. Ces trois formalisations ont été faites en utilisant les assistants de preuves Minlog, Coq et Isabelle/HOL. A partir des preuves formelles, ces systèmes nous ont permis d'extraire automatiquement des programmes. Ces derniers implantent en fait des variantes de l'algorithme bien-connu N.B.E (Normalization By Evaluation). Cette étude de cas nous a permis de tester et comparer les mécanismes d'extraction de ces trois assistants de preuves sur un exemple non-trivial. Les fichiers sources du développement Coq se trouvent ici.

Ce travail est décrit dans un article invité pour le numéro spécial 82 de la revue Studia Logica. Une entrée bibtex.

Traduction des quantificateurs non-calculatoires de Minlog en Coq

Travail commun avec Bas Spitters.

Nous proposons ici un moyen de simuler en Coq les quantificateurs non-calculatoires de Minlog dus à Ulrich Berger. Comme étude de cas pour cet encodage, Nous utilisons une preuve de normalisation à la Tait, ainsi que la concaténation de vecteurs. Moyennant un petit effort d'adaptation, il est effectivement possible de faire disparaître les arguments non-calculatoires des programmes extraits. On obtient alors du code extrait qui est non seulement plus proche du code attendu, mais aussi plus rapide et moins gourmand en mémoire. Enfin, nous avons noté que cette traduction correspond en fait à une vision monadique, ce qui nous a amené à étudier les relations entre formules de Harrop, logique modale dite "lax", et la théorie des types de Coq.

Un rapport technique sur ce sujet.

L'extraction de la formalisation FTA

Travail commun avec Luis Cruz-Filipe.

Dans ces travaux, nous avons essayé d'utiliser le mécanisme d'extraction de Coq sur la formalisation FTA. Ce FTA, ou "Théorème Fondamental de l'Algèbre", stipule l'existence de racines complexes pour tout polynômes complexes non-constants. Cette formalisation a été réalisée à Nimègue, et fait maintenant parti du projet plus vaste C-CoRN. Le défi est donc d'obtenir un programme concret de recherche de racines en utilisant l'extraction sur cette formalisation mathématique. Jusqu'à maintenant, cet objectif n'a pas été atteint, mais des résultats intermédiaires intéressants ont été obtenus.

Un article sur ces travaux a été accepté à la conférence Calculemus'05. Une version préliminaire de cet article, ainsi qu'une entrée bibtex.

Des foncteurs pour les preuves et les programmes

Travail commun avec Jean-Christophe Filliâtre.

Nous utilisons ici le système de modules de Coq ainsi que l'extraction pour certifier la librairie standard Set de Ocaml. Un article sur ce travail a été accepté à la conférence ESOP'04.

  • Le postscript de cet article, une entrée bibtex.
  • Les fichiers sources ainsi que plus de précisions sont disponibles ici.

Une nouvelle extraction pour Coq

Ce travail a débuté en tant que stage de DEA au LRI, avec Christine Paulin comme encadrant. Le sujet initial était: Exécution de termes de preuves Coq.

J'ai ensuite poursuivi mes recherches sur le sujet dans le cadre d'une thèse, toujours encadré par Christine Paulin. Cette thèse a combiné des considérations théoriques ainsi que la réalisation d'une implantation.

  • Mon manuscrit de thèse au format postscript ou pdf. Une entrée bibtex. Une traduction anglaise de ce manuscrit est maintenant disponible ici. Vu la qualité actuelle de cette traduction, tout relecteur serait le bienvenu!

Au cours de ma thèse, j'ai présenté des résultats intermédiaires pendant la conférence TYPES'2002 à Berg en Dal, près de Nimègue, Pays-Bas, en avril 2002.

  • Les transparents de cette présentation, à visionner avec Active-Dvi.
  • L'article accepté ultérieurement pour publication dans les actes de la conférence. Une entrée bibtex.

Formalisation de l'algorithme de Stålmarck en Coq

Stage de maîtrise à l' INRIA Sophia Antipolis.

Vieillerie : un travail scolaire sur les systèmes dynamiques

Une petite étude de la fonction logistique f : x -> rx(1-x), dans le cadre des TIPE de prépas.

[LogisticFunction]
  • En Word, ou en zip exécutable (45 Ko).
  • Ce travail est maintenant disponible également en LaTeX: ps ou pdf.
    Exercice: comparer les deux versions (doc/tex) et deviner pourquoi la plupart des scientifiques utilisent LaTeX...
  • Quelques images.
  • Une courte bibliographie: doc, ps, pdf.