The pi.r2 project is a joint research team between Inria and Université Paris-Diderot. We are physically located on the university campus inside Paris. Among other research activities, our team is leading the development of the Coq proof assistant. Coq is a free software resulting from more than twenty years of R&D, allowing to mechanically guarantee mathematical proofs or computer programs. The usage of Coq is now widespread, with a large user community and many major results already proven with it. Coq has recently received two ACM prizes. At the same time, Coq remains a research platform that allows many experiments and evolves constantly.
As part of the ADT ("Action de Développement Technologique") Coq-API, we are offering a 2-year position for a specialized engineer. Her/His task will be to refactor and improve the inner modular design of Coq, and highlight the API of its various components.
Even if Coq can already be highly customized by a user (for instance via a macro language and a plugin system), its current success leads to even more needs in terms of access to the different internal layers of the system: we want to allow the developments of all kinds of third-party contributions that extend Coq or interact with it. But currently, the internal components of Coq are poorly documented and/or organized. The recruited engineer will re-design the interfaces of the internal components of Coq, and document these interfaces. Moreover (s)he will also contribute to the development life of Coq, for instance via the creation or improvement of specific tools meant for development support (test framework, external proof checker, package manager...)
We are looking for an OCaml expert. A prior knowledge of Coq usage and concepts is also deeply desired. Any experience in other proof assistants (as user or developer) will be taken in account favorably. The principles of software engineering should be mastered, as well as the standard tools for software projects (vcs, dependencies, tests, debug, profiling...). Some system administration skills will also be helpful (in relation with the test framework).
Through the official webpage of this job offer, or via email email@example.com