I am a senior researcher at INRIA in Paris, France.
(Here are directions to our site, and here is a map.)
I am a member of the Gallium team.
Those who would give up essential Liberty, to purchase a little
temporary Safety, deserve neither Liberty nor Safety.
-- Benjamin Franklin (1755)
Current software (gitlab):
- Menhir, a LR(1) parser generator for the
OCaml programming language;
- visitors, an OCaml syntax extension
that generates object-oriented visitors for traversing and transforming data structures
an OCaml library for ML type inference and elaboration,
described in my ICFP 2014 paper.
a simple OCaml module for computing
the least fixed point of a system of monotone equations;
an OCaml adaptation of Wadler's and Leijen's prettier printer;
a Coq library for dealing with binding using de Bruijn indices
a Coq library for writing a do/while loop, while producing
clean OCaml extracted code.
My current and former Ph.D. students are: