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 342EB7F7AF; Mon, 5 Oct 2015 14:58:54 +0200 (CEST) IronPort-PHdr: 9a23:yCUswxDJBR3KnwUW3Up2UyQJP3N1i/DPJgcQr6AfoPdwSP/5p8bcNUDSrc9gkEXOFd2CrakU16yI4+u9ByQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkb7isMCNKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgKK4jM4U34K2k5DCg3BqRX7RYvZsy3gt+M71jPMeYXxRrkxXXGg6K1wYB7ukiYOcTAjtCnYhtY2g7pfiBOkrhM5zZSHTpuSMa9bf6jdcNdSYGNcWNcZAylACYOxa80KBvcHLM5VqZLhrh4WpAG/HhWhD+OpxCUe1Sy+5rEzz+l0SVKO5wcnBd9b9S2M9Ng= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michel.mauny@ensta-paristech.fr; spf=Pass smtp.mailfrom=michel.mauny@ensta-paristech.fr; spf=Pass smtp.helo=postmaster@ns4.ensta.fr Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of michel.mauny@ensta-paristech.fr) identity=pra; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="michel.mauny@ensta-paristech.fr"; x-sender="michel.mauny@ensta-paristech.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of michel.mauny@ensta-paristech.fr designates 147.250.10.4 as permitted sender) identity=mailfrom; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="michel.mauny@ensta-paristech.fr"; x-sender="michel.mauny@ensta-paristech.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@ns4.ensta.fr designates 147.250.10.4 as permitted sender) identity=helo; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="michel.mauny@ensta-paristech.fr"; x-sender="postmaster@ns4.ensta.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DDAQDnchJWlwQK+pNdg3tugmW3CoYKIYV5AoEwPBABAQEBAQEBARABAQEBAQgWB0+CHYIIAQEEDBdOBxEJHAIFFgsCAgkDAgECAUUGAQkDCAEBEAeIEw2KLp00k38MIIEihVGKEoJpgUMFjQWId4UXhCeFL0eDcYcrijuDbQI4glIdgUBvAYg+AQEB X-IPAS-Result: A0DDAQDnchJWlwQK+pNdg3tugmW3CoYKIYV5AoEwPBABAQEBAQEBARABAQEBAQgWB0+CHYIIAQEEDBdOBxEJHAIFFgsCAgkDAgECAUUGAQkDCAEBEAeIEw2KLp00k38MIIEihVGKEoJpgUMFjQWId4UXhCeFL0eDcYcrijuDbQI4glIdgUBvAYg+AQEB X-IronPort-AV: E=Sophos;i="5.17,638,1437429600"; d="scan'208";a="181133702" Received: from ns4.ensta.fr ([147.250.10.4]) by mail2-smtp-roc.national.inria.fr with ESMTP; 05 Oct 2015 14:58:53 +0200 Received: from ns4.ensta.fr (localhost [127.0.0.1]) by ns4.ensta.fr (Postfix) with ESMTP id 3ECBDF2CCA; Mon, 5 Oct 2015 14:58:53 +0200 (CEST) X-Virus-Scanned: amavisd-new at ns4.ensta.fr Received: from ns4.ensta.fr ([127.0.0.1]) by ns4.ensta.fr (ns4.ensta.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id MULSsKIwhJki; Mon, 5 Oct 2015 14:58:51 +0200 (CEST) Received: from zemail.ensta.fr (zemail.ensta.fr [147.250.1.16]) by ns4.ensta.fr (Postfix) with ESMTP id 1B975F2CCD; Mon, 5 Oct 2015 14:58:51 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 128E02975AC; Mon, 5 Oct 2015 14:58:51 +0200 (CEST) Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id 17nhIlIPtt1j; Mon, 5 Oct 2015 14:58:50 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 3F1C629785C; Mon, 5 Oct 2015 14:58:50 +0200 (CEST) X-Virus-Scanned: amavisd-new at zemail.ensta.fr Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id xhl-9Prh-PP0; Mon, 5 Oct 2015 14:58:50 +0200 (CEST) Received: from pcmm.ensta.fr (wifianasys.ensta.fr [147.250.35.53]) by zemail.ensta.fr (Postfix) with ESMTPS id 221F62975AC; Mon, 5 Oct 2015 14:58:50 +0200 (CEST) References: <558AB211.1030901@ensta-paristech.fr> To: Caml List , ocaml-jobs@inria.fr, gdr.gpl@imag.fr From: Michel Mauny X-Enigmail-Draft-Status: N1110 Organization: ENSTA-ParisTech Message-ID: <56127409.2090206@ensta-paristech.fr> Date: Mon, 5 Oct 2015 14:58:49 +0200 User-Agent: Mozilla/5.0 (X11; U; Linux i686; fr; rv:1.8.1.6) Gecko/20070728 Thunderbird/6.0.1 Mnenhy/0.7.5.0 MIME-Version: 1.0 In-Reply-To: <558AB211.1030901@ensta-paristech.fr> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: [Caml-list] [Urgent] Post-doctoral position available at ENSTA-ParisTech - Secure-OCaml project Dear all, Bonjour =C3=A0 tous, Nous avons une offre de postdoc =C3=A0 l'ENSTA-ParisTech, sur le plateau de= Saclay, sur le projet SecurOCaml. Voir ci-dessous une description de l'off= re. N'h=C3=A9sitez pas =C3=A0 transmettre cette offre aux candidats qu'elle= pourrait int=C3=A9resser. We have a post-doctoral position available at ENSTA-ParisTech (Palaiseau, F= rance), to be filled as soon as possible, on the Secure-OCaml project. See = below for more information. Sorry for multiple postings and don't hesitate to transfer this announce to= whom could be interested. (**************************************************************************= ** * Fran=C3=A7ais (See below for an english version.) **************************************************************************= **) Type d'offre : post-doctorant Lieu de travail : ENSTA-ParisTech, Palaiseau Dur=C3=A9e : de 12 =C3=A0 24 mois Date de d=C3=A9but : d=C3=A8s que possible Salaire : entre 2200 =E2=82=AC et 2400 =E2=82=AC nets par mois (s=C3=A9curi= t=C3=A9 sociale incluse) Th=C3=A8mes : Langages de programmation, compilation, typage, OCaml Mission : concevoir et r=C3=A9aliser des biblioth=C3=A8ques permettant de v= =C3=A9rifier des propri=C3=A9t=C3=A9s de s=C3=BBret=C3=A9 et de s=C3=A9curi= t=C3=A9 de codes et donn=C3=A9es charg=C3=A9es dynamiquement par des applic= ations OCaml. Descriptif du poste : Le projet Secure-OCaml (FUI18) a pour objectif d'adap= ter le langage OCaml au d=C3=A9veloppement d'applications pr=C3=A9sentant d= es enjeux de s=C3=A9curit=C3=A9. Le projet r=C3=A9unit les partenaires indu= striels et acad=C3=A9miques suivants : OCamlPro, SafeRiver, LexiFi, TrustIn= Soft, INRIA, ENSTA-ParisTech, CEA, et Trusted Labs. Parmi les objectifs du projets Secure-OCaml, la fiabilit=C3=A9 du traitemen= t des donn=C3=A9es et codes charg=C3=A9s dynamiquement est un enjeu particu= li=C3=A8rement important : en effet, le typage statique effectu=C3=A9 par l= e compilateur OCaml fournit des garanties fortes aux applications. En revan= che, lors du chargement dynamique d'un code ou d'une donn=C3=A9e, une appli= cation n'a aucune l'assurance que ce code ou cette donn=C3=A9e est conforme= aux hypoth=C3=A8ses qu'elle fait. La mission du post-doctorant sera d'=C3=A9tudier ces probl=C3=A8mes et d'y = apporter des solutions qui seront rendues librement disponibles sous forme = de biblioth=C3=A8ques. Ce travail sera r=C3=A9alis=C3=A9 en =C3=A9troite coop=C3=A9ration avec INR= IA-Paris et OCamlpro SAS. Profil recherch=C3=A9 : - comp=C3=A9tences fortes en typage et compilation - go=C3=BBt affirm=C3=A9 pour le d=C3=A9veloppement OCaml - la connaissance de la cha=C3=AEne de compilation d'OCaml est un atout s= uppl=C3=A9mentaire Contexte de travail : l'ENSTA-ParisTech est une Grande =C3=89cole d=E2=80= =99ing=C3=A9nieurs g=C3=A9n=C3=A9raliste, localis=C3=A9e =C3=A0 Palaiseau, = sur un campus qu'elle partage avec l'=C3=8Bcole Polytechnique. L'=C3=A9quip= e =C2=AB S=C3=BBret=C3=A9 et Fiabilit=C3=A9 des Logiciels =C2=BB (http://u2= is.ensta-paristech.fr/groups/SL/) de l'Unit=C3=A9 d'Informatique et d'Ing= =C3=A9nierie des Syst=C3=A8mes =C2=BB vise =C3=A0 contribuer =C3=A0 l'am=C3= =A9lioration des techniques de d=C3=A9veloppement, d'analyse et de v=C3=A9r= ification des logiciels. Informations compl=C3=A9mentaires : - michel.mauny ensta-paristech fr - +33 1 8187 2032 Pour candidater, envoyer =C3=A0 michel.mauny ensta-paristech fr = les documents suivants : - CV avec liste de publications - lettre de motivation - coordonn=C3=A9es de deux personnes en mesure de recommander le candidat Les candidatures seront examin=C3=A9es jusqu'=C3=A0 ce qu'un candidat soit = accept=C3=A9. Merci de v=C3=A9rifier sur http://u2is.ensta-paristech.fr/members/mauny/postdoc-secureocaml.txt que l'offre est encore disponible avant de candidater. (**************************************************************************= *** * * Secure-OCaml - Checking safety and security properties of OCaml programs * **************************************************************************= ****) (See french version above) Offer: postdoc Workplace: ENSTA-ParisTech, Palaiseau (see http://www.ensta-paristech.fr/en/getting-ensta-paristech) Duration: from 12 to 24 months Starting: ASAP Salary: from 2200 =E2=82=AC to 2400 =E2=82=AC net per month (incl. social s= ecurity) Mission: design and implement libraries for verifying safety and security p= roperties of dynamically loaded OCaml code and data. Description: The Secure-OCaml project aims at adapting the OCaml language = to the development of applications involving security issues. The project g= athers the following industrial and academic partners: OCamlPro, SafeRiver,= LexiFi, TrustInSoft, INRIA, ENSTA-ParisTech, CEA, and Trusted Labs. Among the objectives of the Secure-OCaml project, the safety of dynamically= loaded code and data is a particularly important issue. In the same way as= static typing ensures safety properties about statically linked code, appl= ications shoould be able to have similar ensurance about dynamically loaded= code and data. The postdoc's mission will be to study these problems and bring effective s= olutions that shall be made freely available to the OCaml community. This work will be realized in cooperation with INRIA-Paris and OCamlpro SAS. Profile sought: - skills in typing and compilation - strong capabilities and taste in functional programming in general and = OCaml in particular - a knowledge of the OCaml compiler is an additional advantage Context of the job: ENSTA-ParisTech is a french (top ten) engineering schoo= ls, located at Palaiseau, on a campus shared with INRIA and Ecole Polytechn= ique. The research group "Software Safety and Reliability of Software" is p= art of ENSTA's Computer Science and System Engineering Department, and aims= at improving techniques of development, analysis and verification of softw= are. For more information, contact: - michel.mauny ensta-paristech fr - +33 1 8187 2032 To apply, send the following documents to michel.mauny ensta-paristech= fr: - your resume, with a list of publications - a motivation letter - the name and address (e-mail) of two persons who could write a recommen= dation Applications will be received as long as the position remains available. Pl= ease check at: http://u2is.ensta-paristech.fr/members/mauny/postdoc-secureocaml.txt that the position is still available. -- Michel Mauny U2IS ENSTA ParisTech, Universit=C3=A9 Paris-Saclay 828, boulevard des Mar=C3=A9chaux F-91762 Palaiseau Cedex +33 1 8187 2032