[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Job description: We are currently looking for a 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 gross salary is 36000 euros per year. 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. Starting date: The starting date will be decided together with the candidate and could not be before March. The contract is for two years. The candidate should contact sacer...@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. -- ---------------------------------------------------------------- Real name: Claudio Sacerdoti Coen Doctor in Computer Science, University of Bologna E-mail: sacer...@cs.unibo.it http://www.cs.unibo.it/~sacerdot ----------------------------------------------------------------