Thierry Cocan | |
---|---|
Thierry Coquand | |
Születési dátum | 1961. április 18. [1] (61 éves) |
Születési hely | Jalieu (Franciaország, Isère megye) |
Ország | Franciaország |
Tudományos szféra | A matematika alapjai , az elméleti számítástechnika |
Munkavégzés helye | Göteborgi Egyetem |
alma Mater | Higher Normal School (Párizs) |
Akadémiai fokozat | PhD |
Akadémiai cím | Egyetemi tanár |
tudományos tanácsadója | Gerard Hue |
Ismert, mint | Konstrukciós kalkulus fejlesztője, a matematika univalens alapjai program társszervezője, értelmetlen topológia kutatója |
Díjak és díjak | Gödel Társaság kutatási díja (2008) |
Médiafájlok a Wikimedia Commons oldalon |
Thierry Coquand ( fr. Thierry Coquand ; 1961. április 18. ) francia matematikus , a típuselmélet és az automatikus bizonyítás specialistája, a konstrukciós kalkulus megalkotója , a matematika egyenértékű alapjait megteremtő program társszervezője . A Göteborgi Egyetem Informatikai és Mérnöki Karának professzora .
Jalieu-ban született ( Isère megye ). 1980-ban a párizsi Higher Normal School -ban érettségizett , 1982-ben letette a "matematikai összesítést" ( fr. agrégation de mathématiques ) - a középiskolai matematikatanítás jogáért versenyvizsgát. 1985-ben védte meg doktori ( PhD ) értekezését számítástechnikából az INRIA -n Gerard Huet irányítása alatt . 1985-1989-ben az INRIA vendégkutatója, 1989-ben kutatási igazgató ( fr. directeur de recherche ).
1990 óta Svédországban él és dolgozik: a Chalmers University of Technology vendégkutatója , 1996-tól pedig a Göteborgi Egyetem professzora .
Míg az 1980-as évek közepén Gérard Huet-tel dolgozott, kifejlesztette a konstrukciós kalkulust, egy magasabb rendű polimorf λ-számítást függő típusokkal , amely a Barendregt λ-kocka legmagasabb pontját foglalja el, majd később a Coq automatikus proof szoftver alapja lett. rendszer . (A "Coq" név elrejti az építési kalkulus rövidítését, a CoC , valamint Kokan vezetéknevének első részét.)
Főbb publikációk a típuselméletről és az automatikus bizonyításról. Az 1990-es és 2000-es évek munkáinak sorozata az értelmetlen topológiának és a konstruktív algebrának szól .
A logikai, módszertani és filozófiai XIV. Nemzetközi Kongresszus programbizottságának tagja (2011, Nancy ).
Vlagyimir Voevodszkijjal és Steve Awodey -vel közösen a 2012-2013-as tanévre egy speciális kutatási programot szervezett az Institute for Advanced Study -ban, a matematika egyenértékű alapjainak szentelve, ennek keretében részt vett a 2012-2013-as tanévre. könyv „Homotópiás típuselmélet: A matematika univalens alapjai”, amely felvázolja a program főbb eredményeit.
A Journal of Functional Programming és a Mathematical Structures in Computer Science folyóiratok szerkesztőbizottságának tagja (mindkettőt a Cambridge University Press adja ki ). A Springer-Verlag és a Princeton University Press konstruktív algebráról és bizonyítási elméletről szóló könyveinek lektora .
2008-ban elnyerte a Gödel Society ( angol Kurt Gödel Society ) jelentős kutatási díját a metrizációs terekkel ( angol space of valueations ) kapcsolatos munkájáért [2] .
2011-ben a Royal Society of Sciences and Letters of Gothenburg ( svédül: Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ) tagjává választották.
Tematikus oldalak | ||||
---|---|---|---|---|
|