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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 59A697EEEF; Wed, 24 Jun 2015 15:35:23 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.national.inria.fr; envelope-from="michel.mauny@ensta-paristech.fr"; x-sender="michel.mauny@ensta-paristech.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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: A0BzAgDosIpVnAQK+pNbg2VfglhGtUCGGoJEgzSBS0wBAQEBAQESAQEBAQEICwkJIS6ENRdOBxocAgUWCwILAwIBAgFLAQkDCAEBEAeIFA2ZR50ZhlSQGYEhjwmDFYFDBYwTh3KEWIQHhCxCg06Ca4wng1oCgQlmDAGCJm0BgkcBAQE X-IPAS-Result: A0BzAgDosIpVnAQK+pNbg2VfglhGtUCGGoJEgzSBS0wBAQEBAQESAQEBAQEICwkJIS6ENRdOBxocAgUWCwILAwIBAgFLAQkDCAEBEAeIFA2ZR50ZhlSQGYEhjwmDFYFDBYwTh3KEWIQHhCxCg06Ca4wng1oCgQlmDAGCJm0BgkcBAQE X-IronPort-AV: E=Sophos;i="5.13,671,1427752800"; d="scan'208";a="137656064" Received: from ns4.ensta.fr ([147.250.10.4]) by mail3-smtp-sop.national.inria.fr with ESMTP; 24 Jun 2015 15:35:22 +0200 Received: from ns4.ensta.fr (localhost [127.0.0.1]) by ns4.ensta.fr (Postfix) with ESMTP id 5436FEC3B3; Wed, 24 Jun 2015 15:35:22 +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 czttm9YmLp4M; Wed, 24 Jun 2015 15:35:16 +0200 (CEST) Received: from zemail.ensta.fr (zemail.ensta.fr [147.250.1.16]) by ns4.ensta.fr (Postfix) with ESMTP id B2573EC3B2; Wed, 24 Jun 2015 15:35:16 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id AB406297228; Wed, 24 Jun 2015 15:35:16 +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 0UV45RyugSxb; Wed, 24 Jun 2015 15:35:15 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id CB25C29727A; Wed, 24 Jun 2015 15:35:15 +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 fArAqdJaQN1J; Wed, 24 Jun 2015 15:35:15 +0200 (CEST) Received: from pcmm.ensta.fr (wifianasys.ensta.fr [147.250.35.53]) by zemail.ensta.fr (Postfix) with ESMTPS id B3D2D297228; Wed, 24 Jun 2015 15:35:15 +0200 (CEST) Received: from [10.0.0.11] ([10.0.0.1]) (authenticated bits=0) by pcmm.ensta.fr (8.14.8/8.14.7) with ESMTP id t5ODZDB1013271 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NO); Wed, 24 Jun 2015 15:35:15 +0200 From: Michel Mauny Reply-To: michel.mauny@ensta-paristech.fr, Michel Mauny To: Caml List , ocaml-jobs@inria.fr Organization: ENSTA-ParisTech Message-ID: <558AB211.1030901@ensta-paristech.fr> Date: Wed, 24 Jun 2015 15:35:13 +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 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: [Caml-list] Post-doctoral position available at ENSTA-ParisTech - Secure-OCaml project Dear all, 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. (**************************************************************************= *** * * Secure-OCaml - Checking safety and security properties of OCaml programs * **************************************************************************= ****) (* * English (Voir plus bas pour une version fran=C3=A7aise.) *) Offer: postdoc Publication date: June 23 2015 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. =20 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. (**************************************************************************= ** * Fran=C3=A7ais (See above for an english version.) **************************************************************************= **) Type d'offre : post-doctorant Date de publication : 23 juin 2015 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. --=20 Michel Mauny michel.mauny ensta.fr ENSTA ParisTech --=20 Michel Mauny ENSTA ParisTech Universit=C3=A9 Paris-Saclay 828, boulevard des Mar=C3=A9chaux 91762 Palaiseau Cedex +33 1 8187 2032