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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id F0BA07ED26 for ; Fri, 1 Jun 2012 04:51:13 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Av8EAEUtyE+CiAFm/2dsb2JhbABEFoU4rl2BB4IZAQUjRgEBHiUCGQ0CAlcGE4gLC6Yakj+BI4luGoRJgRIDliiIFASBVYR4gmKBXQ X-IronPort-AV: E=Sophos;i="4.75,695,1330902000"; d="scan'208";a="146107302" Received: from leb.cs.unibo.it ([130.136.1.102]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 01 Jun 2012 04:51:13 +0200 Received: from ssl.cs.unibo.it (ssl.cs.unibo.it [127.0.0.1]) (Authenticated sender: hidden) by leb.cs.unibo.it (Postfix) with ESMTPSA id 19F8325CE ; Fri, 1 Jun 2012 04:51:03 +0200 (CEST) Message-ID: <1338519434.6612.33.camel@zenone> From: Claudio Sacerdoti Coen To: sacerdot Date: Fri, 01 Jun 2012 04:57:14 +0200 In-Reply-To: <1296059286.27942.41.camel@zenone> References: <1262690107.5919.57.camel@zenone> <1296059286.27942.41.camel@zenone> Organization: Department of Computer Science -- University of Bologna Content-Type: text/plain; charset="UTF-8" X-Mailer: Evolution 3.2.2-1+b1 Content-Transfer-Encoding: 7bit Mime-Version: 1.0 Subject: [Caml-list] Post-Doc positions in the CerCo FET-Open EU Project === Two New Post-Doc positions in the CerCo FET-Open EU Project === ** Job duration: 01/07/2012-30/06/2013 (one year) ** Deadline for reception of candidatures: 29/06/2011 We are currently looking for two Post-Doc positions at the Department of Computer Science, University of Bologna, to work on the CerCo FET-Open EU Project (see description below). The gross salary is 26174 euros per year. Only a minimal amount of taxes is due. The University of Bologna is the oldest running western university and the Department of Computer Science (http://www.cs.unibo.it/en/), located in the historic city center, has strong expertise in theoretical computer science and logic and it participates to several national and international projects. The Post-Doc will join the HELM team, leaded by Prof. Asperti, whose members work in the domains of Type Theory and Mathematical Knowledge Management. The CerCo project is headed by Dr. Sacerdoti Coen. The candidates will benefit from exchange opportunity with the other project participants (University Paris-Diderot, Paris, and University of Edinburgh, Edinburgh). The candidates will not have any teaching duties. Requirements: We are looking for candidates with a Ph.D. in Computer Science and previous experience in Type Theory (in particular Interactive Theorem Proving), and being proficient in functional programming languages. We also accept candidates that will defend their Ph.D. thesis in the near future, if they can provide a formal proof that they will. Starting date: The proposed starting date is the 01/07/2012. The contract is for one year. The candidate should contact sacerdot@cs.unibo.it for further information. Project description: The CerCo FET-Open EU Project is aimed at producing the first _formally_ _verified_ _complexity_preserving_ compiler for a subset of C to the object code for a microprocessor used in embedded systems. The output of the compilation process will be the object code and a copy of the source code annotated with _exact_ computational complexities for each program slice in O(1). The exact computational complexities (expressed in clock cycles and parametric in the program input) can then be used to formally reason on the overall code complexity. The source code of the compiler will be formally verified using the Matita Interactive Theorem Prover (http://matita.cs.unibo.it), based on a variant of the Calculus of (Co)Inductive Constructions. The candidate will contribute to the formal proof of correctness of the compiler. How to submit candidatures: All candidates are invited to get in touch in advance with Dr. Claudio Sacerdoti Coen , submitting a curriculum vitae. The official candidature must be received by standard mail (no electronic submission) before the 29/06/2011. Candidates must fill in the forms (in Italian only) that can be found at the following address: https://www.aric.unibo.it/AssegniRicerca/BandiPubblicati/zz_Bandi_din.aspx (look for the word "Matita" in the second column) Candidates must also attach two recommendation letters. Foreign candidates will be helped in compiling the forms. Kind regards, C.S.C. -- ---------------------------------------------------------------- Real name: Claudio Sacerdoti Coen Doctor in Computer Science, University of Bologna E-mail: sacerdot@cs.unibo.it http://www.cs.unibo.it/~sacerdot ----------------------------------------------------------------