Short bio: I did a PhD from 1995 to 1999 under the supervision of Christine Paulin, regarding verification of imperative programs in the system Coq. Right after my PhD, in fall 1999, I redesigned the architecture of Coq, to isolate a kernel ; this is briefly described in this paper. Then I left for a post-doc at SRI, in the PVS team, where I started the development of the ICS decision procedure. When I returned to France, I started in 2001 the development of a tool for program verification called Why, used for the proof of C programs (in the Caduceus tool, now subsumed by Frama-C) and for the proof of Java programs in the Krakatoa tool. In 2010, the Why tool became Why3.
Publications / Program committees / Doctoral juries
I'm an enthusiastic programmer since 1984 (I was 13). My first computer was a Thomson TO7/70, on which I used to code in Basic and 6809 assembly. In 1986, I switched to an Atari 520 ST, on which I used to code in GFA Basic and in 68000 assembly. In the early 1990s, I progressively moved to PC. Today, I code mostly in OCaml, under Linux. A few years ago, I discovered Project Euler ; if you like mathematics and programming, you'll love it.
I'm the (co)author of the following programs:
I'm teaching compilers at École Normale Supérieure.
I'm teaching INF411 and INF564 at École Polytechnique.
Older teaching material:
My favorite Computer Science books, and why.