My research interests :

  • compilers,
  • programming languages in general; functional languages in particular,
  • Static analysis,
  • Formal methods and mechanized verification in general; verification of programs transformation, translation validation and verified compilers in particular.
  • News

    Ph. D Thesis document

    The documentation of the Coq source code of MLCompCert here. MLCompCert is a mechanically verified front-end for the purely functional fragment of ML to the back-end of CompCert.