Postdoc at Inria/Irisa on translation validation from Liquid Haskell

Project-team TEA (Inria-Rennes, France) is seeking a talented PhD with demonstrated experience in theory and implementation of refinement types in programming, automated verification and proof of programs.

The aim of the post-doctoral project is to design a certified code generator from a system programming DSL defined in Liquid Haskell to an existing verified compiler (CompCert, CakeML, or C*). In the spirit of Pnueli's translation validation principle, we will prove generated code to obey program properties inferred from source programs. We will study extensions to hardware synthesis, dynamic memory management, higher-order functions, etc.

The application deadline is March 24th. 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