Mémoire de DEA, Université Paris 7, septembre 2001 : ps
Thèse de doctorat, Université Paris 11, septembre 2005 : ps.gz, pdf
Raisonnement au premier ordre dans le Calcul des Constructions Inductives
Rapport de Recherche 1380, LRI, decembre 2003 (en anglais) : ps
Ce rapport présente un calcul de séquents sans contraction pour un fragment du Calcul des Constructions Inductives correspondant à la logique intuitionniste du premier ordre. Nous montrons qu'il s'agit d'une extension naturelle du calcul LJT de Dyckhoff et nous démontrons qu'il satisfait les propriétés d'élimination des coupures et des contractions, étendant ainsi les résultats obtenus par Dyckhoff, afin de justifier son utilisation comme base pour des procédures de recherche de preuves. Enfin, nous décrivons les stratégies mises en oeuvre dans l'implantation d'une tactique Coq basée sur ce calcul.
Raisonnement au premier ordre dans le Calcul des Constructions Inductives
in TYPES 2003 : Types for Proofs and Programs, LNCS 3085 , pages 162-177.
© 2004 Springer-Verlag (en anglais): ps
Version abrégée du rapport ci-dessus (en anglais)
in Seizièmes Journées Francophones des Langages Applicatifs.
© 2005 INRIA : ps
En 1989, William Pugh publia un article intitulé Skip lists: a probabilistic alternative to binary trees dans lequel il analysait en détail les performances d'une structure de données mutable appelée skip-list. Cette structure de données permet de représenter un ensemble fini ordonné à l'aide d'une liste chaînée à niveaux dans laquelle chaque élément est situé à un niveau aléatoire. Dans cet article nous décrivons comment une tentative d'implantation en Objective Caml d'une version fonctionnelle de ces listes à niveaux a permis d'identifier une correspondance forte entre cette structure et une structure d'arbres binaires de recherche probabilistes dont nous décrirons l'implantation et les propriétés.
Reflexion de preuves en logique du premier ordre avec égalité (co-écrit avec Évelyne Contejean)
in 20th International Conference on Automated Deduction,
LNAI 3632, pages 7-22.
© 2005 Springer-Verlag (en anglais) : ps,
pdf
Nous présentons un interpréteur de traces de preuve en logique du premier ordre multi-sortée avec égalité. Grâce à l'utilisation de la réflexion dans Coq, nous avons implanté cet interpréteur et prouvé formellement sa correction par rapport à l'interprétation réflexive des formules comme des propositions de Coq à l'intérieur même de la théorie des types de Coq. Ce cadre générique permet d'interpréter des traces de preuve calculée par n'importe quel prouveur automatique, pourvu qu'elles soient suffisamment précises: nous illustrons cela sur des traces de preuve produites par l'outil CiME lorsqu'il résout des problèmes d'unifiablilité grâce à la complétion ordonnée. Nous commentons les résultats obtenus par sur la bibliothèque de problèmes TPTP.
Decider les égalités dans la théorie des constructeurs
in TYPES 2006: Types for Proofs and Programs, LNCS 4502, pages 78-92.
© 2007 Springer-Verlag (en anglais) : pdf
Nous présentons une procédure de décision pour la satisfiabilité d'ensembles finis d'égalités et inégalités dans la théorie des constructeurs: les termes présents peuvent contenir à la fois des symboles de fonction non interprétés et des constructeurs. Les constructeurs sont des symboles injectifs et des constructeurs distincts donnent des termes eux-mêmes différents. Cela correspond aux propriétés des constructeurs de types (co-)inductifs dans la théorie des types inductifs. Nous le faisons dans un cadre où les symboles de fonctions peuvent être partiellement appliqués et les égalités entres fonctions sont autorisées. Nous décrivons notre algorithme comme une extension de la clôture de congruence et donnons des preuves de terminaison, correction et complétude. Ensuite, nous en discutons les limites et les extensions possibles en décrivant son implantation dans l'assistant de preuve Coq.
Archives collaboratives pour les preuves formelles - Une solution à la Wiki
in Towards Mechanized Mathematical Assistants
14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, proceedings, LNCS 4573, pages 78-92.
© 2007 Springer-Verlag (en anglais) : pdf
Nous présentons un nouveau système pour le développement en ligne de mathématiques formalisées. Ce système permet une collaboration dans le style Wiki et fournit à ses utilisateurs une version mise en page et navigable de leur travail. Nous décrivons un prototype basé sur Coq et l'interface interactive en ligne développée par le second auteur, et une version modifiée du système MediaWiki. Nous présentons les problèmes non résolus tels que les dépendances et la cohérence de l'archive. Nous expliquons les limitations du prototype actuel et donnons des perspectives pour une solution plus robuste.
Ces travaux ont été financés par le Projet Bricks/Focus Project 642.000.501 (Advancing the Real use of Proof Assistants) et le projet FEAR de la NWO.
Un langage de preuve déclaratif pour l'assistant de preuve Coq
in TYPES 2007 : Types for Proofs and Programs, LNCS 4941.
© 2008 Springer-Verlag (en anglais): pdf
Aussi dans Theorem Proving in
Higher-Order Logics : Emerging Trends Proceedings
Technical report 364/07, Computer Science Department,
University of Kaiserslautern
Cet article présente un nouveau langage de preuve pour l'assistant de preuve Coq. Ce langage utilise le style déclaratif. Son but est d'être une alternative simple, naturelle et robuste au langage Ltac existant. Nous décrivons la syntaxe de notre langage, puis nous donnons une description informelle de ses commandes et une sémantique opérationnelle. Nous expliquons comment ce langage pourrait être utilisé pour implanter les squelettes de preuve formelles. Enfin, nous présentons les fonctionnalités que nous souhaitons implémenter ultérieurement.
Poster - Bricks midterm Symposium ps.gz (A3) pdf
Un vrai Web Sémantique pour les Mathématiques mérite une vraie sémantique (avec Herman Geuvers, Cezary Kaliszyk, James McKinna et Freek Wiedijk)
in Proceedings of the 3rd Semantic Wiki Workshop
SemWiki 2008 -- The Wiki Way of Semantics (en anglais):
SALTed PDF
Les documents mathématiques, ainsi que leur instrumentation par les ordinateurs, sont riches en structure, tant au niveau de la présentation, des méta-données que de la sémantique, commes objets dans un système pour la logique mathématique formelle. Les outils du Web Sémantique implantent les deux premiers niveaux, tandis que les assistants de preuve s'en tiennent au troisième, typiquement avec des approches ad hoc pour les deux premiers. Notre thèse est qu'un Web des documents, définitions et preuves mathématiques doit être assorti d'une sémantique de plein droit, au sens du troisième niveau. Nous proposons un "MathWiki" pour enrichir les outils du Web 2.0 avec la sémantique précise des Assistants de preuves actuels.