[TYPES/announce] PhD position in programming languages and formal proof

[Randy Pollack]

	  Certified Complexity Preserving Compiler (CerCo):
	  Programming and proving a compiler in Type Theory

For details contact Randy Pollack <rpollack at 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.