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.
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 CSC_41011 (formerly INF411) and INF564 at École Polytechnique.
Older teaching material:
My favorite Computer Science books, and why.
