For some of them, a more detailed description can be found below.
2019-today
2016-today
2015-2018
2000-2018
2008
2006
2005
2004
2002
2000
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.
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.
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.
Stage de maîtrise à l'INRIA Sophia Antipolis.