Thierry Coquand har tilldelats Kurt Gödel Centenary Research Prize Fellowship

Nyhet: 2008-05-27

Pris för bevis 

Thierry Coquand vid Data- och informationsteknik, Göteborgs universitet, har tilldelats Kurt Gödel Centenary Research Prize Fellowship om 120.000 dollar för sin nyskapande forskning inom matematikens grunder. Priset är personligt och tillfaller en senior forskare i världen vars forskning har sitt ursprung i Gödels arbete inom matematik och logik.

Personliga priser är ovanliga i forskarvärlden och särskilt inom forskning om matematikens grunder. Att prisas som senior forskare vid 47 års ålder visar att det har gått fort för Thierry Coquand. Han studerade matematik och logik vid Ecole Normale Superieure i Paris och doktorerade i datavetenskap vid forskningsinstitutet INRIA. Redan 1996 utnämndes han till professor i datalogi vid Göteborgs Universitet. 2001 fick han ta emot Wallmarkska priset av Kungliga Vetenskapsakademin.

Förhållandet mellan datorprogram och matematiska bevis

Thierry Coquands forskning befinner sig i gränslandet mellan matematisk logik och teoretisk datavetenskap och är av grundläggande eller primär natur. Vilken är strukturen på matematiska bevis? Finns det kopplingar mellan matematiska bevis och datorprogram? Ett av Thierrys forsningsområden är typteori, som bygger på Bertrand Russells filosofiska reflektioner och är den mest exakta formuleringen av logik. Samtidigt tycker han att det finns spännande och intressanta tillämpningar trots ämnets och områdets grundläggande natur.

Felfritt intressant inom mjukvaruutveckling

I Frankrike har ett system utvecklats som bygger på Thierrys idéer för att kontrollera bevis. Forskare vid Microsoft Research i Paris har använt programmet för att formalisera ett mycket känt problem och bevis, fyrfärgsteoremet. Att Microsoft är intresserade av ett matematiskt bevis kan tyckas förvånande, men de tror att det kan öka förståelsen för hur man utvecklar en korrekt programvara. Samma system har också använts för att bekräfta att chipet i ett betalkort inte innehåller fel, eller buggar. Typteori har också tillämpningar inom lingvistik och spelar en viktig roll för institutionens forskning i språkteknologi, eftersom typteori gör det möjligt att automatiskt översätta språkfragment med bibehållen mening och korrekt grammatik.

Thierry bor sedan 18 år i Sverige och uppskattar bredden och djupet på forskningen vid Institutionen för data- och informationsteknik, som är gemensam mellan Chalmers och Göteborgs universitet.

- Förvånande nog är mina kollegors forskning om programmeringsspråk och funktionell programmering relevanta för att förstå matematikens grunder, säger han, samtidigt som matematikens grunder är viktig inom datavetenskap.

Priset fick Thierry ta emot av Österrikes forskningsminister vid en ceremoni i Wien i april i år.

Kurt Gödel Society främjar forskning inom logik, filosofi och matematisk historia och även andra områden som Kurt Gödel var verksam inom. Gödel var 1900-talets största logiker vars forskning har bidragit till förståelsen av matematikens grunder, han är mest känd för sin ofullständighetssats.

INRIA står för Institute National de Recherche en Informatique et en Automatique.

Länk till Kurt Gödel Centenary Research Prize Fellowship

AV:
031-772 4891