[ 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>.

Reply via email to