From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 17ECF7FA43; Fri, 18 Jul 2014 11:58:17 +0200 (CEST) X-IronPort-AV: E=Sophos;i="5.01,684,1400018400"; d="scan'208";a="85889482" Received: from zmbs3.inria.fr ([128.93.142.16]) by mail2-relais-roc.national.inria.fr with ESMTP; 18 Jul 2014 11:58:16 +0200 Date: Fri, 18 Jul 2014 11:58:16 +0200 (CEST) From: Pierre Letouzey To: coq-club@inria.fr, caml-list@inria.fr Message-ID: <130852054.4002204.1405677496813.JavaMail.zimbra@inria.fr> In-Reply-To: <433161342.3992210.1405676907764.JavaMail.zimbra@inria.fr> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Originating-IP: [82.225.151.49] X-Mailer: Zimbra 8.0.6_GA_5922 (ZimbraWebClient - FF24 (Linux)/8.0.6_GA_5922) Thread-Topic: 2-year position for a specialized engineer (Inria Project pi.r2, ADT Coq-API) Thread-Index: s7ooeLCeNAbFQO0tLe15nyBjtS5hww== Subject: [Caml-list] 2-year position for a specialized engineer (Inria Project pi.r2, ADT Coq-API) 2-year Position for a Specialized Engineer (Inria Project pi.r2, ADT Coq-AP= I) ---------------------------------------------------------------------------= -- Html version of this email: http://www.pps.univ-paris-diderot.fr/~letouzey/coq-api-position.html =3D=3D Context =3D=3D The pi.r2 project [1] is a joint research team between Inria [2] and Univer= sit=E9 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 resea= rch platform that allows many experiments and evolves constantly. =3D=3D Mission =3D=3D As part of the ADT ("Action de D=E9veloppement 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. =3D=3D Job Description =3D=3D 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...) =3D=3D Profile =3D=3D 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). =3D=3D Job Details =3D=3D * Required diploma: Master 2 or Engineer or PhD * Required experience: at least 2 years, or a PhD * Salary: slightly above an Inria "ing=E9nieur de recherche" with the corre= sponding experience =3D=3D Contact =3D=3D Through the official webpage [5] of this job offer, or via email: coq-api@i= nria.fr =3D=3D References =3D=3D [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-rech= erche-et-developpement-confirmes-et-specialistes/%28view%29/details.html?nP= ostingTargetID=3D14562