The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

I am pleased to announce the availability of 1 or 2 postdoc positions 

for the project "CoqHoTT: Coq for Homotopy Type Theory",

funded by an ERC Starting Grant.

Expected start: between October 2017 and March 2018.

This 5-year project concerns the development of a new generation of

proof assistants based on the fascinating connection between homotopy

theory and type theory. 

The different axes of the project are described at

http://coqhott.gforge.inria.fr/

I am seeking exceptional candidates who are interested (and who

preferably have a proven track record) in one or more of the following

topics:

- Homotopy Type Theory

- Interactive Theorem Proving in Coq, Agda or Lean

- Development of (part of) a proof assistant, or its extensions.

Successful applicants will join the Inria Gallinette Team,

led by me, at Inria, Nantes. The financial conditions of 

the post-doc are standard Inria conditions. 

Previous postdocs in the project have

included Pierre-Marie Pédrot, Benedikt Ahrens (ending in september 2017)

and Eric Finster (still in the project).

*Application deadline*: Sept 15.  If you are interested in joining the

CoqHoTT team and want to learn more about the project, please contact

me directly at nicolas.tabareau AT inria.fr.  To apply for a postdoc position,

please send me a CV, research statement, and list of references.

For further information, see the project web page at:

http://coqhott.gforge.inria.fr/

Best regards,

Nicolas Tabareau