[TYPES/announce] Postdoc position in the FP7 CerCo Project

[Claudio Sacerdoti Coen]

           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
<sacerdot at cs.unibo.it> (in CC Paolo Tranquilli <tranquil at cs.unibo.it>)
for further informations and assistance in the compilation of the forms.

-- 
----------------------------------------------------------------
Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: sacerdot at cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------