Publications
Submitted/unpublished manuscripts
. Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory, PDF
. From Axioms to Rewriting Rules. .pdf Table with results detailed by domains.
. Normalization in Supernatural deduction and in Deduction modulo , 2010. .pdf
Accepted (Journals and Conferences)
Accepted (Workshops)
. Translating HOL to Dedukti, presented at the workshop PxTP'15. EPTCS
. A Shallow Embedding of Resolution and Superposition Proofs into the lamdba-Pi-Calculus Modulo, presented at the PxTP'13 workshop. .pdf
. CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo, presented at the PxTP'12 workshop. .pdf
. Consistency Implies Cut Admissibility, presented at the workshop on PSATTT'11, available through HAL.
. How can we prove that a proof search method is not an instance of another? 2009. Presented by Gilles Dowek at the workshop LFMTP'09. .pdf DOI
. An abstract completion procedure for cut elimination in deduction modulo 2006. Short presentation given at LICS'06. .pdf
The rare LaTeX sources here are incomplete (the included files are absent), they are given in case they are more readable than other formats.
See also my publication list on HAL (not up-to-date).
Talks
A short presentation of my thesis for the école jeunes chercheurs en programmation : .pdf .tex
A longer presentation, with the work done during my master, and then introducing the ideas of the completion in deduction modulo : .pdf .tex
The short presentation given at LICS'06, introducing completion in deduction modulo : .pdf .tex
The slides for the LFCS'07 talk (Cut elimination in deduction modulo by abstract completion): .pdf .tex
The slides for the CSL'07 talk (Unbounded proof-length speed-up in deduction modulo): .pdf .tex
Some presentation of the encoding of functional Pure Type Systems in superdeduction: .pdf .tex
The slides of my PhD defense « Good Proofs in Deduction Modulo »: .pdf
Reports
Master's thesis
I did it in March/August 2005 in the team PROTHEO at the LORIA. It was on the application of Abstract Canonical Systems framework to the standard completion (a.k.a. Knuth-Bendix completion) and to natural deduction. This framework, introduced by N. Dershowitz and C. Kirchner, is a theoretical approach of completion procedures and of other procedures working by saturation. It is based on the introduction of some order over the proofs. This order is used to represent the intuitive notion of "good proofs" by minimal proofs. I proved that standard completion was an instance of this framework, and that we can generalize this framework somehow to capture the natural deduction too.
Report
My stage of maîtrise
I did it in January/March 2004 at the Lehrstuhl Broy of the Department of Informatics of the Technische Universität München. It dealt with the automatic generation of programs through examples. For instance, 1+0=1 and 2+3=5 permit to generate the addition, the "simplest" program which satisfies these constraints. My approach was to extend G. Huet's higher order unification algorithm.
Results
- The program to
generate programs through examples. After decompression,
type
makeand pry. (Sorry, no tutorial available.) - The report (.ps)
- And the sources. (Need the program sources for the appendix.)
My stage of licence
I did it in June/July 2003 in the team PROTHEO at the LORIA. It was on the use in equational logic (where one consider only universally quantified equalities between terms) of probabilities in the same way they were introduced by J. Halpern for first order logic.
