[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Certified Complexity Preserving Compiler (CerCo): Programming and proving a compiler in Type Theory For details contact Randy Pollack <rpoll...@inf.ed.ac.uk>. ** This is restricted to EU students. ** A 3 year PhD studentship is available in a project titled "A Certified Complexity Preserving Compiler" (CerCo), funded by the European Commission under "Future and Emerging Technologies" (FET). The studentship will be held within the Laboratory for Foundations of Computer Science, at the School of Informatics, University of Edinburgh, to begin in 2010, start date flexible. 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 used in embedded systems. The work comprises the definition of cost models for the input and target languages, coding the compiler in Type Theory and the machine-checked proof of preservation of complexity (concrete, not asymptotic) along compilation, using the *Matita* proof tool. The compiler will return 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. The permanent researchers involved in the CerCo project are Randy Pollack in Edinburgh, Andrea Asperti and Claudio Sacerdoti-Coen in Bologna and Roberto Amadio and Yann Regis-Gianas in Paris. The Edinburgh site will focus on the compiler front end. We are interested in use of dependent types in programming as well as in proof. Suitable candidates will have a strong first degree in Computer Science and a strong interest in formal proof and type theory. Candidates are encouraged to contact Randy Pollack to informally discuss the project further. Formal application will be through the School's normal PhD application process: <http://www.inf.ed.ac.uk/postgraduate/phd.html> -- Randy Pollack Phone: +44 131 650 5145 URL: http://homepages.inf.ed.ac.uk/rpollack Edinburgh University, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.