To content
Read more about how we use cookies on gu.se
# Thierry Coquand has been awarded the Kurt Gödel Centenary Research Prize Fellowship

## Prize-winning proof

## The relationship between computer programs and mathematical proof

## Aiming at fault-free software development

## Contact Information

### Catharina Jerkbrant, Communications officer

News: May 27, 2008

Thierry Coquand, of the Department of Computer Science and Engineering, University of Gothenburg, has been awarded the 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.

Personal awards are uncommon in the world of research, and especially within research into the foundations of mathematics. Being acclaimed as a senior researcher at the age of 47, shows how rapidly Thierry Coquand has become a prominent figure. He studied mathematics and logic at the Ecole Normale Superieure in Paris and gained a PhD in computer science at INRIA, the research institute. He was made a professor of computer science at Göteborg University as early as 1996. In 2001 he was awarded the Wallmark Prize by the Royal Swedish Academy of Sciences.

Thierry Coquand's research straddles the boundary between mathematical logic and theoretical computer science, and is of a fundamental, or primary, nature. What is the structure of mathematical proof? Are there links between mathematical proof and computer programs? Type theory is one of Thierry's research fields. This builds upon Bertrand Russell's philosophical reflections and is the most exact expression of logic. At the same time, he believes that there are exciting and interesting applications, despite the fundamental nature of the subject and field.

A system that builds upon Thierry's ideas about checking proof has been developed in France. Workers at Microsoft Research in Paris have used the program to formalise a well-recognised problem and proof - the four colour theorem. It may seem somewhat surprising that Microsoft are interested in mathematical proof, but they believe that it can improve our understanding of how to develop correct software programs. The same system has also been used to confirm that debit card chips do not contain faults, or bugs. Type theory also has applications in linguistics and has an important role in the faculty's research into language technology, because type theory makes it possible to translate language segments automatically, whilst retaining meaning and correct grammar.

Thierry has lived in Sweden for 18 years and appreciates the breadth and depth of research at the Department of Computer Science and Engineering, which is a joint faculty of Chalmers and Göteborg University.

He says: "Surprisingly enough, my colleagues' research into programming languages and functional programming is relevant to the understanding of the foundations of mathematics, whilst at the same time, the foundations of mathematics are important for computer science."

Thierry received the prize from Austria's minister of research at a ceremony in Vienna this April.

The Kurt Gödel Society promotes research into logic, philosophy and the history of mathematics, and also into other fields in which Kurt Gödel worked. Gödel was the twentieth century's greatest logician, and his research has improved the understanding of the foundations of mathematics. He was most renowned for his incompleteness theorems.

INRIA stands for the Institute National de Recherche en Informatique et en Automatique.

IT Faculty, SE-412 96 Göteborg, SWEDEN

Visiting Address:

Lindholmsplatsen 1

Phone:

+46 (0)31 772 4898, +46 (0)766 18 27 48