I am a research engineer working on Programming Languages and Tools in the FLaRe team.

I have a degree in computer science and hold a PhD from the Ecole Polytechnique in Saclay, France on the study of the meta-theory behind proof assistant and Pure Type Systems.

Before joining Facebook, I spent some time in Chalmers, Sweden, to work on the formalization of linear algebra algorithms, and then spent the last 6 years in a french startup called ProvenRun, working on the design and proof of correctness of an industrial grade embedded Operating System.

Interests

Type systems, proofs of programs, higher order logic and dependent types