coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Post Doctoral Position in Formalization of Mathematics

From: Thierry Coquand <coquand AT chalmers.se>
To: "types-list AT lists.seas.upenn.edu" <types-list AT lists.seas.upenn.edu>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Post Doctoral Position in Formalization of Mathematics
Date: Mon, 20 Sep 2010 12:03:24 +0200
Accept-language: en-US, sv-SE
Acceptlanguage: en-US, sv-SE

We seek PhDs with a strong interest in functional programming,

type theory and formal representation of proofs in type theory.

This position is within a Strep Open, 7th framework, which involves, as other sites,INRIA, INRIA-microsoft, Nijmegen and La Roja, see

http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath

One main part of this work will be to explore the feasibility of representing simple mathematical algorithms (in linear algebra and algebraic topology) using the ssreflect extension of type theory developed in the Mathematical Components project.

For more information, see

http://ledig-anstallning.adm.gu.se/detail.php?lt_id=6465

[Coq-Club] Post Doctoral Position in Formalization of Mathematics, Thierry Coquand