From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 E8E3B7ED5C; Fri, 3 Aug 2012 05:03:58 +0200 (CEST) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of sacerdot@cs.unibo.it) identity=pra; client-ip=130.136.1.102; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="sacerdot@cs.unibo.it"; x-sender="sacerdot@cs.unibo.it"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of sacerdot@cs.unibo.it designates 130.136.1.102 as permitted sender) identity=mailfrom; client-ip=130.136.1.102; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="sacerdot@cs.unibo.it"; x-sender="sacerdot@cs.unibo.it"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@leb.cs.unibo.it) identity=helo; client-ip=130.136.1.102; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="sacerdot@cs.unibo.it"; x-sender="postmaster@leb.cs.unibo.it"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Av4CACM+G1CCiAFmgWdsb2JhbABFDgiFZbMpIgEBFiYngkpGAQFDAiYCcogNm2+OQZMrgSGKJhqFWIESA5ZciBsEgVqHJjuBXQ X-IronPort-AV: E=Sophos;i="4.77,704,1336341600"; d="scan'208";a="152337730" Received: from leb.cs.unibo.it ([130.136.1.102]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 03 Aug 2012 05:03:58 +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 6B9E72525 ; Fri, 3 Aug 2012 05:03:52 +0200 (CEST) Message-ID: <1343963424.3889.45.camel@zenone> From: Claudio Sacerdoti Coen To: poplmark@lists.seas.upenn.edu. Date: Fri, 03 Aug 2012 05:10:24 +0200 Organization: Department of Computer Science -- University of Bologna Content-Type: text/plain; charset="UTF-8" X-Mailer: Evolution 3.4.3-1 Mime-Version: 1.0 Content-Transfer-Encoding: 7bit Subject: [Caml-list] Postdoc position in the FP7 CerCo Project New postdoc position in the FP7 CerCo Project Job description: We are currently looking for a one year (or less) Post-Doc position at the Department of Computer Science, University of Bologna, to work on the CerCo FET-Open EU Project (see description below). The candidate can either contribute to the formal verification (in Matita) of the CerCo complexity preserving compiler or he can study the application to more complex scenarios of the technique employed to provide exact cost estimation of the execution time of programs. The gross salary is 26174 euros per year. Only a mimal amount of taxes are due on it (net salary about 1900 euros per month). The tentative starting date is the middle of September 2012. The University of Bologna is the oldest 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 candidate will benefit from exchange opportunity with the other project participants (University Paris-Diderot, Paris, and University of Edinburgh, Edinburgh). The candidate will not have any teaching duties. Requirements: Candidates should have a Ph.D. in Computer Science and previous experience in either Type Theory (in particular Interactive Theorem Proving) or Compiler Development, and being proficient in functional programming languages. Candidates who have not defended their Ph.D. yet but are supposed to do that soon will also be considered. Project description: The CerCo FET-Open EU Project (http://cerco.cs.unibo.it) 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. Application details: To apply some forms in Italian only must be filled in, signed, and sent by courier. They must arrive before the 10th of September. The candidates should contact in advance Claudio Sacerdot Coen (in CC Paolo Tranquilli ) for further informations and assistance in the compilation of the forms. -- ---------------------------------------------------------------- Claudio Sacerdoti Coen Doctor in Computer Science, University of Bologna E-mail: sacerdot@cs.unibo.it http://www.cs.unibo.it/~sacerdot ----------------------------------------------------------------