[PRL] Fwd: [TYPES/announce] Certified Complexity at PPS (Paris): Post-Doc + PhD

[Mitchell Wand]

This certainly looks cool.

---------- Forwarded message ----------
From: Roberto Amadio <Roberto.Amadio at pps.jussieu.fr>
Date: Mon, Nov 16, 2009 at 9:37 AM
Subject: [TYPES/announce] Certified Complexity at PPS (Paris): Post-Doc +
PhD
To: types-announce at lists.seas.upenn.edu


[ The Types Forum (announcements only),
    http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


 CerCo positions at PPS

A PhD and a one year post-doc positions are available to work in Paris, in
the PPS laboratory, on the EU-FP7 Certified Complexity project (CerCo).

The CerCo project aims at the construction of a formally verified complexity
preserving compiler from a large subset of the C programming language to
some typical micro-controller assembly language, of the kind traditionally
used in embedded systems. The work comprises the definition of cost models
for the input and target languages, and the machine-checked proof of
preservation of complexity (concrete, not asymptotic) along compilation. The
compiler will also return tight and certified cost annotations for the
source program, providing a reliable infrastructure to draw temporal
assertions on the executable code, while reasoning on the source. The
compiler will be open source, and all proofs will be public domain.

A short and preliminary scientific description of the project is available
here <http://www.pps.jussieu.fr/%7Eamadio/cerco-desc.pdf>

The permanent researchers involved in the CerCo project are Andrea Asperti
and Claudio Sacerdoti-Coen in Bologna, Randy Pollack in Edinburgh, and
Roberto Amadio and Yann Régis-Gianas in Paris. The Paris site will focus in
particular on the construction of a prototype of the cost annotating
compiler and on the construction of a semi-automatic tool to draw complexity
assertions on the execution time of C programs.

A strong background in functional programming, compiler construction, and
machine-assisted proof methods is expected. For more information, potential
candidates may contact Roberto Amadio
<http://www.pps.jussieu.fr/%7Eamadio/>or Yann
Régis-Gianas <http://www.pps.jussieu.fr/%7Eyrg/>. These positions are
expected to be filled around February 2010. The gross salary is expected to
be 45KEuros/year for the post-doc and 30 KEuros/year for the doctoral
student. Interested applicants should send a .tar file to Roberto Amadio
including: (1) their letter of interest, (2) their curriculum vitae, and (3)
contact information of 2-3 professional references.

Up-to-date information on these positions will be made available at this
address <http://www.pps.jussieu.fr/%7Eamadio/cerco-positions.html>.
-------------- next part --------------
HTML attachment scrubbed and removed