Le mécanisme d'extraction de Coq permet de transformer des preuves Coq en programmes fonctionnels. Cet article a pour but d'illustrer 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.

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.

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.

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.

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.

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.

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.

• Le rapport final de ce stage.

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.

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

• Le rapport.
• Les sources Coq de la première version, et leur diagramme (Miroir de cette URL).
• Une nouvelle version de ce travail, due à Laurent Théry:
  • Les sources Coq.
  • Une interface en ligne pour jouer avec le programme Ocaml extrait.
  • L'article commun décrivant cette nouvelle implantation. Une entrée bibtex
  • Cet article a été présenté lors de la conférence TPHOLs'2000 à Portland, Oregon, en août 2000. Les présents…

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

• En word.
• En pdf après passage ultérieur à LaTeX. Exercice: comparer ces deux versions et deviner pourquoi la plupart des scientifiques utilisent LaTeX…
• Quelques images.
• Une courte bibliographie: doc ou pdf.