Short bio: I did a PhD from 1995 to 1999 under the supervision of Christine Paulin, regarding verification of imperative programs in the system Rocq (formely know as the Coq proof assistant). Right after my PhD, in fall 1999, I redesigned the architecture of Rocq 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, a prototype of SMT solver. When I returned to France, I started in 2001 the development of a tool for program verification, known today as 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.
I'm the author with Sylvain Conchon of the book Learn Programming with OCaml.
Older teaching material:
My favorite Computer Science books, and why.
