coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] post-doc for CertiCoq project

From: Greg Morrisett <morrisett AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] post-doc for CertiCoq project
Date: Tue, 20 Oct 2015 11:54:13 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=morrisett AT gmail.com; spf=Pass smtp.mailfrom=morrisett AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f45.google.com
Ironport-phdr: 9a23:VwUkwBT7qrX7v4Dncrp0bLlc9dpsv+yvbD5Q0YIujvd0So/mwa64ZxON2/xhgRfzUJnB7Loc0qyN4/2mATRLv83JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviptuLO04W33KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA5iBdHSy3C9gv7RZrtrmOus+1nwiiBMNHqZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==

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

[Coq-Club] post-doc for CertiCoq project, Greg Morrisett, 10/20/2015