Version 1 (modified by sacerdot, 9 years ago) (diff)



The School of Informatics in the University of Edinburgh is one of the largest and most successful computing departments in the UK, as borne out by the latest UK Research Assessment Exercise (2008) which showed the School had a a significantly larger volume of research rated internationally excellent (3*) or world leading (4*) than any other university in the UK. The School has world-class research institutes in the areas of theoretical computer science, computing systems architecture, artificial intelligence and cognitive science.

This project will be carried out in the Laboratory for Foundations of Computer Science (LFCS) (, a research group in theoretical computer science, with expertise in areas including Logic and Semantics (Prof.�Gordon�Plotkin), Complexity (Dr. Kousha Etessami, Dr. Mary Cryan), Programming Languages (Prof.�Philip�Wadler) and Databases (Prof.�Peter Buneman). The LFCS has a long history of work on computer assisted proof, including the development of foundational type theories such as the Edinburgh Logical Framework, and the Extended Calculus of Constructions. The LFCS has also worked on tools for machine proof, including the proof assistant LEGO, and Proof General, a generic front-end for proof assistants.

Also part of Edinburgh School of Informatics is the Institute for Computing Systems Architecture, with expertise in advanced compilers (Prof. Michael O'Boyle).

Role in the project and main tasks

The UEDIN site will lead the Work Package 3 on the certification of the front end of the CerCo? compiler. It will also actively contribute to the development of the unverified prototype compiler in WPround(1+1:0).

Relevant previous experience (resource analysis)

  • EU Project IST-2001-33149 MRG on Mobile Resource Guarantees (2003) (member).
  • EU Project IST-15095 MOBIUS on Mobility, Ubiquity and Security (2005) (member)
  • EPSRC funded project EP/C537068/1 ReQueST on Resource Quantification in eScience Technologies (2005)

Staff members involved (UEDIN)

Robert Pollack Research Fellow, University of Edinburgh
Post Doc (24 months) to be hired during year 1
PhD Student (36 months) to be hired

Key person at UEDIN

Dr. Robert Pollack is a world expert in computer assisted proof and proof assistants. He has a long history of contributions in the application of type theory. In the late 1980s he developed the LEGO system at Edinburgh. More recently, Dr.�Pollack has worked on several formalization projects, including a formalization of the fundamental theorem of algebra and investigations into ways to represent modularity and binding structure. He was on the steering committee of the EU Coordination Action 510996 TYPES, and involved in several previous EU actions.

For 17 years he worked as a software engineer specialized in real-time systems, in particular industrial process control and air traffic control. On these topics he had been Consultant to the Transportation Systems Center of the U.S. Department of Transportation, and chief software engineer of a startup company building process control computers.

Recent publications related to the project comprise:

  1. Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich. Engineering formal metatheory. In Principles of Programming Languages (POPL), pp.�3-15, IEEE 2008.
  2. Thierry Coquand, Randy Pollack, Makoto Takeyama. A Logical Framework with Dependently Typed Records. Fundam. Inform. 65(1-2): 113-134, 2005.