jacques-henri.jourdan [at] normalesup [dot] org
I am currently a postdoc at Max Plank Institute for Software Systems (MPI-SWS) in Derek Dreyer's team, on the RustBelt project. Our objective is to formalize Rust's type system and prove that some particular unsafe Rust code fragments do not break the whole type system
My research interests include formal verification of software. In particular, my PhD project lies exactly between abstract interpretation and the Coq proof assistant.
I am also interested in several subjects linked to programming languages: LR parsing, floating-point arithmetic, compilation...
My PhD thesis is available here. Its title is "Verasco: a Formally Verified C Static Analyzer".
It received the 2016 thesis prize of the GdR GPL (french research group on programming and software engineering)!
statistical memory profiler for OCaml. It provides
OCaml developers a flexible tool for understanding the
memory behavior of an OCaml program with virtually no
overhead. It can be used through
I am an occasional contributor to the CompCert verified compiler. In particular, I am the initial author of its parser, and I contributed to its support of IEEE754-compliant floating-point numbers.
I was the teaching assistant for the course "Langages de programmation et compilation", at ENS with Jean-Christophe Filliâtre, years 2013/2014 and 2014/2015.
I have been one of the organizers of the Junior Seminar of Inria Paris
I am a member of the France-IOI association since a few years now. I used to participate to the organization of the French Bebras contest contest, which aims at popularizing computer science for teenagers.