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

[Roberto Amadio]

  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 --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20091116/3dbcdd2a/attachment.htm