[Caml-list] 2-year position for a specialized engineer (Inria Project pi.r2, ADT Coq-API)

[Caml-list] 2-year position for a specialized engineer (Inria Project pi.r2, ADT Coq-API)

[Pierre Letouzey]

2-year Position for a Specialized Engineer (Inria Project pi.r2, ADT Coq-API)
-----------------------------------------------------------------------------

Html version of this email:
http://www.pps.univ-paris-diderot.fr/~letouzey/coq-api-position.html

== Context ==

The pi.r2 project [1] is a joint research team between Inria [2] and Université
Paris-Diderot [3]. 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 [4]. 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.

== Mission ==

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.

== Job Description ==

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...)

== Profile ==

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).

== Job Details ==

* Required diploma: Master 2 or Engineer or PhD
* Required experience: at least 2 years, or a PhD
* Salary: slightly above an Inria "ingénieur de recherche" with the corresponding experience

== Contact ==

Through the official webpage [5] of this job offer, or via email: coq-api@inria.fr

== References ==

[1] http://www.pps.univ-paris-diderot.fr/pi.r2
[2] http://www.inria.fr/en/institute/inria-in-brief/inria-in-a-few-words
[3] http://www.univ-paris-diderot.fr/english
[4] http://coq.inria.fr
[5] http://www.inria.fr/institut/recrutement-metiers/offres/ingenieurs-recherche-et-developpement-confirmes-et-specialistes/%28view%29/details.html?nPostingTargetID=14562