The CoqHoTT Project

Engineer position available for ERC CoqHoTT

I am pleased to announce the availability of an engineer position for the project "CoqHoTT: Coq for Homotopy Type Theory", funded by an ERC Starting Grant.

Expected start: October 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

I am seeking exceptional candidates who are interested (and who preferably have a proven track record) in one or more of the following topics: The task of the engineer will be to improve the Template Coq platform and backport recent prototypes made by the CoqHoTT team to this platform. Successful applicants will join the Inria Gallinette Team, led by me, at Inria, Nantes.

*Application deadline*: August 15. If you are interested in joining the CoqHoTT team and want to learn more about the project, please contact me directly at

To apply for an engineer position, please send me a CV and list of references.

For further information, see the project web page at: Best regards, Nicolas Tabareau