usr.lmf.cnrs.fr

Research

I'm senior researcher at CNRS. I work in the Laboratoire Méthodes Formelles (CNRS / Université Paris-Saclay / ENS Paris-Saclay / INRIA Saclay - Île-de-France). I'm doing research in deductive program verification.

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 and this talk. 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.

Publications

Programming

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:

Many other libraries and applications on my github page and on that page dedicated to OCaml programming.

Teaching

I'm teaching compilers at École Normale Supérieure.

I'm teaching CSC_41011 and CSC_52064 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.

On break, continue, and return.

Read the original on usr.lmf.cnrs.fr ↗