===== Recherche ===== ==== Liste des travaux ==== {{page>en:users:letouzey:science#summary_of_works&noheader}} ==== 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'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 [[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]]. Le [[https://www.irif.fr/~letouzey/download/examples_CiE2008.v|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 [[http://www.cs.ru.nl/~freek/comparison/index.html|Freek]], celle de [[http://www.informatik.uni-trier.de/~ley/db/conf/tphol/lncs3600.html|DBLP]], et un [[https://www.irif.fr/~letouzey/download/coq17provers.pdf|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 [[https://www.irif.fr/~letouzey/download/tait.tgz|ici]]. Ce travail est décrit dans un article invité pour le numéro spécial 82 de la revue [[http://www.studialogica.org/|Studia Logica]]. Une entrée [[https://www.irif.fr/~letouzey/bib6.txt|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 [[https://www.irif.fr/~letouzey/download/Letouzey_Spitters_05.pdf|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 [[http://c-corn.cs.kun.nl|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 [[http://imps.mcmaster.ca/calculemus-2005/|Calculemus'05]]. Une version [[https://www.irif.fr/~letouzey/download/lcf_pl_extr05.pdf|préliminaire]] de cet article, ainsi qu'une entrée [[https://www.irif.fr/~letouzey/bib5.txt|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 [[http://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.html|Set]] de OCaml. Un article sur ce travail a été accepté à la conférence [[http://www.cis.ksu.edu/santos/esop2004/|ESOP'04]]. * Le [[http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz|postscript]] de cet article, une entrée [[https://www.irif.fr/~letouzey/bib3.txt|bibtex]]. * Les fichiers sources ainsi que plus de précisions sont disponibles [[http://www.lri.fr/~filliatr/fsets/|ici]]. ==== Une nouvelle extraction pour Coq ==== Ce travail a débuté en tant que stage de DEA au [[http://www.lri.fr|LRI]], avec Christine Paulin comme encadrant. Le sujet initial était: //Exécution de termes de preuves Coq//. * Le [[https://www.irif.fr/~letouzey/download/rapport_dea.ps.gz|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 [[https://www.irif.fr/~letouzey/download/these_letouzey.ps.gz|postscript]] ou [[https://www.irif.fr/~letouzey/download/these_letouzey.pdf|pdf]]. Une entrée [[https://www.irif.fr/~letouzey/bib4.txt|bibtex]]. Une traduction anglaise de ce manuscrit est maintenant disponible [[https://www.irif.fr/~letouzey/download/these_letouzey_English.ps.gz|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 [[http://www.cs.kun.nl/fnds/TYPES2002/|TYPES'2002]] à Berg en Dal, près de Nimègue, Pays-Bas, en avril 2002. * Les [[https://www.irif.fr/~letouzey/download/extraction2002-slides.dvi|transparents]] de cette présentation, à visionner avec [[http://gallium.inria.fr/advi|Active-Dvi]]. * L'[[https://www.irif.fr/~letouzey/download/extraction2002.ps.gz|article]] accepté ultérieurement pour publication dans les actes de la conférence. Une entrée [[https://www.irif.fr/~letouzey/bib2.txt|bibtex]]. ==== Formalisation de l'algorithme de Stålmarck en Coq ==== Stage de maîtrise à l'[[http://www-sop.inria.fr|INRIA Sophia Antipolis]]. * Le [[https://www.irif.fr/~letouzey/stalmarck/rapport.ps.gz|rapport]]. * Les [[https://www.irif.fr/~letouzey/stalmarck/index.html|sources Coq]] de la première version, et leur diagramme (Miroir de cette [[http://www-sop.inria.fr/croap/CFC/stalmarck|URL]]). * Une nouvelle version de ce travail, due à [[http://www-sop.inria.fr/lemme/stalmarck/|Laurent Théry]]: * Les [[https://www.irif.fr/~letouzey/download/stal-new.tar.gz|sources Coq]]. * Une [[http://www-sop.inria.fr/cgi-bin/lemme/stalmarck/run|interface]] en ligne pour jouer avec le programme Ocaml extrait. * L'[[https://www.irif.fr/~letouzey/download/stalmarck.ps.gz"|article]] commun décrivant cette nouvelle implantation. Une entrée [[https://www.irif.fr/~letouzey/bib.txt|bibtex]] * Cet [[https://www.irif.fr/~letouzey/download/stalmarck.ps.gz|article]] a été présenté lors de la conférence [[http://www.cse.ogi.edu/tphols2000|TPHOLs'2000]] à Portland, Oregon, en août 2000. Les [[https://www.irif.fr/~letouzey/pic/tphols.jpg|présents]]... ==== 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. {{https://www.irif.fr/~letouzey/pic/iterati3.gif}} * En [[https://www.irif.fr/~letouzey/download/logistic.doc|word]]. * En [[https://www.irif.fr/~letouzey/download/logistic.pdf|pdf]] après passage ultérieur à LaTeX. Exercice: comparer ces deux versions et deviner pourquoi la plupart des scientifiques utilisent LaTeX... * Quelques [[https://www.irif.fr/~letouzey/download/figures.zip|images]]. * Une courte bibliographie: [[https://www.irif.fr/~letouzey/download/biblio.doc|doc]] ou [[https://www.irif.fr/~letouzey/download/biblio.pdf|pdf]].