From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 C1119820A1; Mon, 2 Sep 2013 13:30:39 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.89,1006,1367964000"; d="scan'208";a="31163658" Received: from sac057r.vpn.inria.fr (HELO [128.93.182.57]) ([128.93.182.57]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 02 Sep 2013 13:30:39 +0200 Message-ID: <522476E6.5010509@inria.fr> Date: Mon, 02 Sep 2013 13:30:46 +0200 From: Bruno Barras User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130803 Thunderbird/17.0.8 MIME-Version: 1.0 To: caml-list@inria.fr, coq-club@inria.fr, agda@lists.chalmers.se, types@lists.chalmers.se Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Subject: [Caml-list] Coq-related postdoc position at Inria-Saclay The Paral-ITP Project (French ANR funding) is looking for candidates for a 1 year post-doc position, to begin as soon as possible, at Inria-Saclay, France. * Position description: The Paral-ITP Project aims at exploiting the potential of multi-core processors to improve the user interaction with highly trustable interactive proof assistants. See the Paral-ITP website for more information (link below). The position is focused on the implementation of a distributed kernel for the Coq proof assistant which would feature the verification of independent proof-checking tasks concurrently. * Context : The successful candidate will work under the supervision of Bruno Barras and collaborate with Enrico Tassi on the Ecole Polytechnique campus. He will also have contacts with other teams of the Paral-ITP Project, namely Fortesse (LRI, Orsay) and Pi.r2 (Inria, Paris). * Requirements: Candidates should have a Ph.D. in Computer Science (or give evidence that the defense is planned soon). They should also be familiar with a proof assistant in type theory (preferably Coq, Agda or Matita) and be experienced in the development in a functional programming language (ML, Haskell). The expertise in concurrency paradigms and the ability to produce high quality code will be important criteria. * Application: Applicants should send an email to Bruno Barras (bruno.barras@inria.fr) including a CV, a list of publications, and a short (two pages at most) statement about their research activities. It may also include the names of up to 2 references. The deadline for applications is September 15, 2013. Notifications of acceptance or rejection will be sent out no later than September 30. * Links: http://paral-itp.lri.fr/ http://www.inria.fr/centre/saclay