[TYPES/announce] post-doc position for CertiCoq project

[Greg Morrisett]

We're looking to hire a post-doc for the CertiCoq project:

  https://academicjobsonline.org/ajo/jobs/6543

The goal of CertiCoq is to build a compiler for Coq within Coq, as an
alternative to the "extraction" mechanism, and to verify the correctness of
the compiler.

There are many interesting things to explore, from advanced optimizations
enabled by the linguistic structure of Gallina, to foundational questions
about how to preserve dependent-types through compilation.

You can find out more about the project here:

  http://www.cs.princeton.edu/~appel/certicoq/

Please apply or consider pointing your brilliant students our way!

Greg Morrisett
Cornell University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20151020/386e1d6f/attachment.html>