My research interests :
programming languages in general; functional languages in particular,
Formal methods and mechanized verification in general;
verification of programs transformation, translation validation and verified compilers in particular.
Ph. D Thesis document
The documentation of the Coq source code of
MLCompCert is a mechanically verified front-end for the purely
functional fragment of ML to the back-end of CompCert.