Curriculum vitae

Birth date: 17 May 1966

Work Address:
      Projet CROAP
       INRIA Sophia Antipolis
       2004, route des Lucioles BP 93
       06902 Sophia Antipolis Cedex, France.

Home Address:
     3 rue du Migrainier, 06600 Antibes, France.

Education:
   1986-1990: Student at `Ecole Normale Supérieure Saint-Cloud'.
   1989-1993 PhD thesis at INRIA Sophia Antipolis in Gilles Kahn's group.

Job:
  1992-1993 Research Assistant at the university of Cambridge in Mike Gordon's group
  1993-1994 PostDoct at Bell  Laboratories in Dave MacQueen's group.
  1994-         Research Assistant at INRIA Sophia Antipolis.
 

Research interests:

• Integration of proving and computing: With John Harrison we have shown how a physical link between Hol and Maple could be exploited to perform safe computations. More recently I've been working on certifying efficient implementations of standard algorithms of computer algebra systems using the Coq system.
• Proof environment: I'm interesting in user interfaces for theorem provers. In my phD thesis I present a generic architecture to build proof environments and I propose different techniques to improve the man-machine interaction while doing proofs.The proof by  pointing allows the user to use the goal as a menu to perform proof steps. The textual explanation provides  a more intuitive representation of formal proofs in a pseudo-natural language. This work has lead to an interface Chol for the theorem prover HOL.
• Programming environment: I've been working on a  prototype programming environment CtCaml for the language Caml. It main purpose was to show in what extends the type information in functional language could be used  in a programming environment.