coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Postdoc at Inria/Irisa on translation validation from Liquid Haskell

From: Jean-Pierre Talpin <jean-pierre.talpin AT inria.fr>
To: <coq-club AT inria.fr>, <haskell AT haskell.org>, <announcements AT lists.artist-embedded.org>, <gdr.gpl AT imag.fr>, <concurrency AT listserver.tue.nl>, <fmics AT inrialpes.fr>, <tccn AT COMSOC.ORG>, <seworld AT sigsoft.org>
Subject: [Coq-Club] Postdoc at Inria/Irisa on translation validation from Liquid Haskell
Date: Sat, 4 Mar 2017 15:53:32 +0100 (CET)

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

[Coq-Club] Postdoc at Inria/Irisa on translation validation from Liquid Haskell, Jean-Pierre Talpin, 03/04/2017