Thierry Coquand

Thierry Coquand
Thierry Coquand, 20 juni 2006.
Född	18 april 1961 (63 år) Isère, Frankrike
Medborgare i	Frankrike
Utbildad vid	École normale supérieure
Sysselsättning	Matematiker, datavetare, ingenjör
Arbetsgivare	Göteborgs universitet Chalmers tekniska högskola INRIA
Utmärkelser
ACM Software System Award (2013)
Redigera Wikidata

Thierry Coquand, född den 18 april 1961 i Jallieu, Isère, Frankrike, är professor i data- och informationsteknik vid Göteborgs universitet.

Biografi

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. 2008 tilldelades han Kurt Gödel Centenary Research Prize Fellowship. 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.

Forskning

Thierry Coquands forskning befinner sig i gränslandet mellan matematisk logik och teoretisk datavetenskap och är av grundläggande eller primär natur, av typen: "Vilken är strukturen på matematiska bevis?" och "Finns det kopplingar mellan matematiska bevis och datorprogram?". Ett av Thierrys forskningsområden är typteori, som bygger på Bertrand Russells filosofiska reflektioner och är den mest exakta formuleringen av logik.

Arv

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 chippet 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.