Kurt Gödel Centenary Research Prize Fellowship to Thierry Coquand

This is not really a very recent piece of news, but I became aware of it only a few days ago and, as far as I can tell, it is news that has not been covered in (TCS) blogs.

Thierry Coquand, of the Department of Computer Science and Engineering, University of Gothenburg, has been awarded a senior Kurt Gödel Centenary Research Prize Fellowship of 120,000 US dollars for his pioneering research into the foundations of mathematics. The prize is personal and is a global award made to a senior researcher, whose work builds on Gödel's achievements in mathematics and logic.

To my mind, it is not so surprising that the recipient of such a prestigious award in logic is a computer scientist. Logic is the calculus of computer science, and researchers like Thierry Coquand work at the boundary between mathematical logic and theoretical computer science. Thierry's research deals with big foundational questions such as:

• What is the structure of mathematical proof?
  
• Are there links between mathematical proof and computer programs?
  

Some of his answers to these foundational questions are at the core of the Coq theorem prover, a proof assistant that has been used to give, amongst other things, a fully machine-checked proof of the four-colour theorem.

Amongst his many achievements, Thierry Coquand also solved a long-standing open problem in measure theory, namely how to define in a purely inductive fashion the measure of Borel sets.

Congratulations to Thierry!