During my Master internship and my PhD (both supervised by G. Dowek), I worked on proof theory.
We defined, with Gilles, the λ Π-calculus modulo, a logical framework with dependent types in which theories are expressed within rewrite rules instead of axioms. And we proved that the root-logical framework of the Coq proof assistant (the Calculus of Constructions) can be embedded as a theory in λ Π-calculus modulo. This led to the implementation of dedukti, a external proof-checker based on λ Π modulo, whose aim is to check proofs developed in various proof assistants (dedukti currently supports proofs coming from Coq and HOL-light).
Thereafter, I proposed the first completeness theorem for strong normalization. Following the work of Gödel for consistency, and using Tait-Girard's reducibility method, I defined a pre-Heyting algebra such that the theories in (minimal) deduction modulo for which one can build a model valued on this algebra, are exactly the ones that enjoy strong normalization. This leads to wonder about independency of particular rewrite rules concerning strong normalization (as Gödel's completeness theorem led to prove independency, concerning consistency, of the axiom of choice from Zermelo-Fraenkel set theory).

When I was working as an expert research engineer at INRIA-MSR joint lab, I was in charge of the development of the TLA proof manager. TLA is a logic, defined by L. Lamport, for specifying and reasoning about concurrent and reactive systems. The proof manager is a system which computes proof obligations that ensure validity of a TLA+ proof, and send those obligations to various external solvers, like Zenon, CVC3 and Isabelle. A main part of my work has been to extend K. Chaudhuri's work from the theoretical part (adding support for some TLA+ features) to the user-oriented part (linking the proof manager to the toolbox IDE, adding memoïzation of proof obligations, etc…). If you're interested in using the proof manager, you may have a look at the tutorial I wrote.

I'm now working on linking Coq and Alt-ergo, the SMT-solver developed by S. Conchon and E. Contejean. This work relies on S. Lescuyer's ergo coq tactic and has two goals: first, certify with Coq Alt-ergo's results, and second, bring the power of SMT-solvers into Coq.

Publications

Slides (selected)

Tutorial on TLAPS (slides by S. Merz)
given at Integrated Formal Methods 2010.

On proof terms for deduction modulo
given for deducteam seminar.

Complete reducibility candidates
given for PSTT09 workshop in Montréal.

Models and Proof Normalization
given for my PhD defense at École Polytechnique.

Embedding Pure Types Systems in λΠ modulo
given for TLCA07 conference in Paris.

Posters

Research

Poster on TLAPS
presented at MSR-INRIA 2011 forum.

Popular science (in french)

Poster on small worlds
Fête de la science, Paris Diderot University.

Poster on compiling
Fête de la science, Paris Diderot University.

I have been involved in the development of a few softwares.
From the theoritical foundation (dedukti) to implementation (tlapm and alt-ergo_to_coq).

Alt-Ergo to Coq

Alt-ergo_to_coq is a proof-trace system combined with a Coq tactic, for certifying the results of the SMT-solver Alt-ergo. More details coming soon.

TLA+ proof manager

I've been, for two years, in charge of the development of the TLA proof manager. TLA is a temporal logic, defined by L. Lamport, for specifying and reasoning about concurrent and reactive systems. The proof manager is a system which computes proof obligations that ensure validity of a TLA+ proof, and send those obligations to various external solvers, like Zenon, CVC3 and Isabelle. A main part of my work has been to extend K. Chaudhuri's work from the theoretical part (adding support for some TLA+ features) to the user-oriented part (linking the proof manager to the toolbox IDE, adding memoïzation of proof obligations, etc…). If you're interested in using the proof manager, you may have a look at the tutorial I wrote.

dedukti

dedukti is a universal proof checker based on λΠ modulo and developed by M. Boespflug. The Embedding of Pure Type Systems in λ Π calculus modulo led to the development of CoqInE, a proof translator from Coq to dedukti, developed by G. Burel.

(This part is intentionally written in french.)

Paris Sud

Je suis en charge des deux groupes de travaux pratiques du cours "Mathématiques pour l'informatique" (Info 229).

ENSIIE

Intervenant du cours "Modèles de calcul".
Slides du chapitre Complexité.
Slides du chapitre λ-calcul simplement typé.
Les notes de cours d'Alexandre Miquel que j'ai utlisées pour la partie sur le théorème d'incomplétude de Gödel.

Paris Diderot

Durant mon monitorat entre 2006 et 2009, j'ai assuré des cours et travaux pratiques de système, programmation java et programmation web en licence à l'Université Paris Diderot. Certains de ces cours et énoncés de travaux pratiques se trouvent ici.

Web

Unlike my previous website or tlaps website, this site is not entirely hand-written from scratch.
I used a very nice template from webdesigneraid.com. This template is distributed under GPL licence.
I also used sometimes Drupal

• for Coq site with J-M. Notin and P-Y. Strub,
• for Corias site with G. Faure,
• for Dedukti site.

Icons

Trying to convey a concept through a single image is a very interesting challenge.
I've made corias and dedukti logos and a proposal of logo for ocsigen (a cam(e)l in an @).

• Image 1
• Image 2
• Image 3