[Haskell-cafe] Postdoc at Inria/Irisa on translation validation from LiquidHaskell

[Ranjit Jhala]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170225/04b6a182/attachment.html>