Publications
Manuscrits soumis/non publiés
. Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory, PDF
. From Axioms to Rewriting Rules. .pdf Tableau des résultats détaillés par domaines.
. Normalization in Supernatural deduction and in Deduction modulo , 2010. .pdf
Acceptées (Journaux et conférences)
Acceptées (Workshops)
. Translating HOL to Dedukti, présenté au workshop PxTP'15. EPTCS
. A Shallow Embedding of Resolution and Superposition Proofs into the lamdba-Pi-Calculus Modulo, présenté au workshop PxTP'13. .pdf
. CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo, présenté au workshop PxTP'12. .pdf
. Consistency Implies Cut Admissibility, présenté au workshop PSATTT'11, disponible via HAL.
. How can we prove that a proof search method is not an instance of another? 2009. Présenté par Gilles Dowek au workshop LFMTP'09. .pdf DOI
. An abstract completion procedure for cut elimination in deduction modulo 2006. Présentation courte à LICS'06. .pdf
Les rares sources LaTeX accessibles ici sont incomplètes (il manque les fichiers d'entête), elles sont données uniquement au cas où elles seraient plus lisibles que les autres formats.
Voir également mes publications sur HAL (pas à jour).
Présentations
Tout d'abord, une courte présentation de mon sujet de thèse pour l'école jeunes chercheurs en programmation : .pdf .tex
Une présentation plus longue, reprenant le travail effectué pendant mon mastère, puis introduisant les idées concernant la complétion en déduction modulo : .pdf .tex
La présentation courte donnée à LICS'06, introduisant la complétion en déduction modulo : .pdf .tex
Les transparents de la présentation pour LFCS'07 (Élimination des coupures en dédution modulo par complétion abstraite) : .pdf .tex
Les transparents de la présentation pour CSL'07 (Réduction de la taille des preuves en déduction modulo) : .pdf .tex
Une présentation de l'encodage des systèmes de type purs fonctionnels en superdeduction: .pdf .tex
Les transparents de ma soutenance de thèse « Bonnes démonstrations en déduction modulo » : .pdf
Rapports
Mon Stage de Mastère
Je l'ai effectué en mars/août 2005 dans l'équipe PROTHEO du LORIA. Il portait sur des application du cadre des systèmes canoniques abstraits à la complétion standard (plus connue sous les jolis noms de Knuth-Bendix) et à la déduction naturelle. Ce cadre, introduit par N. Dershowitz et C. Kirchner, est une approche théorique des procédures de complétion et autres procédures similaires qui fonctionnent par saturation. Il est basé sur l'utilisation d'un ordre sur les preuves, ce qui permet de traduire la notion intuitive de "bonne preuve" par celle de preuve minimale. J'ai montré que la complétion standard rentrait bien dans ce cadre, et qu'en le généralisant un peu on pouvait aussi y faire entrer la déduction naturelle.
Rapport
Mon Stage de MIM2
Je l'ai effectué en janvier/mars 2004 à la Lehrstuhl Broy du Département Informatique de l'Université Technique de Munich. Il portait sur la génération automatique de programmes à partir d'exemples. Par exemple, 1+0=1 et 2+3=5 permettent de générer l'addition, le programme le "plus simple" qui satisfait ces contraintes. Mon approche a été d'étendre l'algorithme d'unification d'ordre supérieure de G. Huet.
Résultats
- Le programme permettant de
générer des programmes à partir d'exemples. Après décompression, un
simple
makedevrait suffir. (Désolé, pas de tutoriel.) - Le rapport en .ps
- Ainsi que les sources. (Nécessite le programme pour les annexes.)
Mon Stage de MIM1
Je l'ai effectué en juin/juillet 2003 dans l'équipe PROTHEO du LORIA. Il portait sur l'utilisation en logique équationnelle (celle où l'on ne considère que des égalités entre termes quantifiées universellement) de probabilités telles qu'elles ont été introduites par J. Halpern pour la logique du premier ordre.
