Cocan, Thierry
| Thierry Cocan | |
|---|---|
| Thierry Coquand | |
| Datum narození | 18. dubna 1961 [1] (ve věku 61 let) |
| Místo narození | Jalieu (Francie, departement Isère) |
| Země | Francie |
| Vědecká sféra | Základy matematiky , teoretická informatika |
| Místo výkonu práce | Göteborgská univerzita |
| Alma mater | Vyšší normální škola (Paříž) |
| Akademický titul | PhD |
| Akademický titul | Profesor |
| vědecký poradce | Gerard Hue |
| Známý jako | Vývojář stavebního počtu, spoluorganizátor programu univalentních základů matematiky, výzkumník nesmyslné topologie |
| Ocenění a ceny | Cena Gödel Society Research (2008) |
| Mediální soubory na Wikimedia Commons | |
Thierry Coquand ( fr. Thierry Coquand ; narozen 18. dubna 1961 ) je francouzský matematik , specialista na teorii typů a automatický důkaz , tvůrce konstrukčního kalkulu , spoluorganizátor programu pro vytváření univalentních základů matematiky . Profesor na Fakultě informatiky a inženýrství na univerzitě v Göteborgu .
Životopis
Narozen v Jalieu ( departement Isère ). V roce 1980 absolvoval Vyšší normální školu v Paříži , v roce 1982 složil "matematickou agregaci" ( fr. agrégation de mathématiques ) - soutěžní zkoušku pro právo vyučovat matematiku na středních školách. V roce 1985 obhájil doktorskou disertační práci ( PhD ) v oboru informatika na INRIA pod vedením Gerarda Hueta . V letech 1985-1989 byl hostujícím výzkumným pracovníkem na INRIA, v roce 1989 působil jako ředitel výzkumu ( fr. directeur de recherche ).
Od roku 1990 žije a pracuje ve Švédsku : byl hostujícím výzkumným pracovníkem na Chalmers University of Technology a od roku 1996 je profesorem na univerzitě v Göteborgu .
Vědecké práce
Při práci s Gérardem Huetem v polovině 80. let vyvinul konstrukční kalkul, polymorfní λ-počet vyššího řádu se závislými typy , který zaujímá nejvyšší bod v Barendregtově λ-krychli a později se stal základem softwaru Coq pro automatický nátisk . systém . (Jméno „Coq“ skrývá jak zkratku pro stavební kalkul, CoC , tak první část Kokanova příjmení.)
Hlavní publikace o teorii typů a automatickém důkazu. Série prací z let 1990-2000 je věnována nesmyslné topologii a konstruktivní algebře .
Organizační činnost
Člen programového výboru XIV. mezinárodního kongresu o logice, metodologii a filozofii (2011, Nancy ).
Spolu s Vladimirem Voevodskym a Stevem Awodeym spoluorganizoval pro akademický rok 2012-2013 na Institutu pro pokročilé studium speciální výzkumný program věnovaný univalentním základům matematiky , v jehož rámci se podílel na společném vytvoření tzv. kniha „Homotopic Type Theory: Univalent Foundations of Mathematics“, která nastiňuje hlavní výsledky programu.
Člen redakčních rad časopisů Journal of Functional Programming a Mathematical Structures in Computer Science (oba vydává Cambridge University Press ). Recenzent knih o konstruktivní algebře a teorii důkazů pro Springer-Verlag a Princeton University Press .
Ocenění a komunity
V roce 2008 získal hlavní cenu za výzkum od Gödel Society ( anglicky Kurt Gödel Society ) za práci na prostorech metrizací ( anglicky space of valuations ) [2] .
V roce 2011 byl zvolen členem Royal Society of Sciences and Letters of Göteborg ( švédsky: Kungliga Vetenskaps-och Vitterhetssamhället i Göteborg ).
Hlavní publikace
- Thierry Coquand. Analýza Girardova paradoxu (anglicky) // Symposium on Logic in Computer Science (LIS'86), Cambridge, MA, 1986. - Cambridge, MA : IEEE , 1986. - S. 227-236 . — analýza analogie Burali-Fortiho paradoxu pro intuicionistickou teorii Martin-Löfových typů .
- Thierry Coquand, Gerard Huet. The calculus of constructions (anglicky) // Information and Computation . - 1988. - Sv. 76 , č. 2-3 . - S. 95-120 . — ISSN 0890-5401 . - doi : 10.1016/0890-5401(88)90005-3 . — hlavní publikace o počtu struktur.
- Thierry Coquand. Sémantika důkazů pro klasickou logiku (anglicky) // Journal of Symbolic Logic . - 1995. - Sv. 60 , č. 1 . - str. 325-337 . — ISSN 0022-4812 . - doi : 10.2307/2275524 . .
- Thierry Coquand. Sur un théorème de Kronecker dotčený les variétés algébriques (fr.) // Comptes rendus hebdomadaires des séances de l'Académie des sciences . - Paříž, 2004. - Sv. 338 , č . 4 . — S. 291–294 . — ISSN 0001-4036 . - doi : 10.1016/j.crma.2003.12.008 .
- Jejichry Coquad. Teorie typů // Stanfordská encyklopedie filozofie . - Stanford : Stanford University Publishing, 2010. - článek o teorii typů ve Stanford Encyclopedia of Philosophy .
Poznámky
- ↑ Německá národní knihovna , Berlínská státní knihovna , Bavorská státní knihovna , Rakouská národní knihovna Záznam #122538900 // Obecná regulační kontrola (GND) - 2012-2016.
- ↑ Åsa Ekvall. Thierry Coquand získal stipendium Kurt Gödel Centenary Research Prize Fellowship . Univerzita v Göteborgu (6. dubna 2008). Staženo: 1. března 2014.
Odkazy
- Domovská stránka Thierryho Cocana (anglicky) . Staženo: 1. března 2014.
 Tematické stránky | ||||
|---|---|---|---|---|
| ||||