Postdoc on translation and validation from Liquid Haskell, Rennes, France

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:

Comments are closed.