Hi all, Inria Project-team TEA is seeking a talented PhD with demonstrated experience in theory and implementation of refinement types in programming and automated verification and proof of programs. The aim of our post-doctoral project is to design a certified code generator from Liquid Haskell to verified, imperative and functional, compiler suites (CompCert, CakeML). We will start by initially focusing on first-order functions in the absence of dynamic memory management. In the spirit of Pnueli's translation validation principle, we will prove code generated from the code generator to obey program properties inferred from source programs, using refinement reflection. We will study extensions to hardware synthesis as well as dynamic memory management, higher-order functions, etc. For context, details, and application, please visit: https://www.inria.fr/ institut/recrutement-metiers/offres/post-doctorat/sejours- post-doctoraux/(view)/details.html?id=PGTFK026203F3VBQB6G68LONZ&LOV5 =4508&nPostingID=11123&nPostingTargetID=17708