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.

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.