Cocan, Thierry
| Thierry Cocan | |
|---|---|
| Thierry Coquand | |
| Syntymäaika | 18. huhtikuuta 1961 [1] (61-vuotias) |
| Syntymäpaikka | Jalieu (Ranska, Isèren departementti) |
| Maa | Ranska |
| Tieteellinen ala | Matematiikan perusteet, tietojenkäsittelyteoria |
| Työpaikka | Göteborgin yliopisto |
| Alma mater | Higher Normal School (Pariisi) |
| Akateeminen tutkinto | PhD |
| Akateeminen titteli | Professori |
| tieteellinen neuvonantaja | Gerard Huet |
| Tunnetaan | Rakennuslaskennan kehittäjä, matematiikan univalenttien perusteiden ohjelman toinen järjestäjä, turhan topologian tutkija |
| Palkinnot ja palkinnot | Gödel-seuran tutkimuspalkinto (2008) |
| Mediatiedostot Wikimedia Commonsissa | |
Thierry Coquand ( fr. Thierry Coquand ; syntynyt 18. huhtikuuta 1961 ) on ranskalainen matemaatikko , tyyppiteorian ja automaattisen todistamisen asiantuntija, rakennuslaskennan luoja , matematiikan univalenttien perusteiden luomisohjelman toinen järjestäjä . Professori Göteborgin yliopiston informatiikan ja tekniikan tiedekunnassa .
Elämäkerta
Syntynyt Jalieussa ( Isèren departementissa ). Vuonna 1980 hän valmistui Higher Normal Schoolista Pariisissa , vuonna 1982 hän läpäisi "matemaattisen aggregaation" ( fr. agrégation de mathématiques ) - kilpailukokeen oikeudesta opettaa matematiikkaa lukioissa. Vuonna 1985 hän puolusti väitöskirjansa tietojenkäsittelytieteestä INRIA : ssa Gerard Huetin johdolla . Vuosina 1985-1989 hän oli vieraileva tutkija INRIA:ssa, vuonna 1989 hän toimi tutkimusjohtajana ( fr. directeur de recherche ).
Vuodesta 1990 hän on asunut ja työskennellyt Ruotsissa : hän oli vierailevana tutkijana Chalmersin teknillisessä yliopistossa ja vuodesta 1996 lähtien professorina Göteborgin yliopistossa .
Tieteelliset teokset
Työskennellessään Gérard Huetin kanssa 1980-luvun puolivälissä hän kehitti rakennuslaskennan , korkeamman asteen polymorfisen λ-lasken , jolla on riippuvaisia tyyppejä ja joka sijaitsee Barendregtin λ-kuution korkeimmalla pisteellä ja josta tuli myöhemmin Coq - automaattisen todistusohjelmiston perusta. järjestelmä . (Nimi "Coq" kätkee sekä rakennuslaskennan lyhenteen CoC että Kokanin sukunimen ensimmäisen osan.)
Tärkeimmät julkaisut tyyppiteoriasta ja automaattisesta todistuksesta. Sarja 1990-2000-luvun teoksia on omistettu turhalle topologialle ja konstruktiiviselle algebralle .
Organisaatiotoiminta
XIV kansainvälisen logiikan, metodologian ja filosofian kongressin ohjelmakomitean jäsen (2011, Nancy ).
Yhdessä Vladimir Voevodskyn ja Steve Awodeyn kanssa hän organisoi erityistutkimusohjelman lukuvuodelle 2012-2013 Institute for Advanced Studyssa, joka oli omistettu matematiikan yksipuolisille perusteille , ja sen puitteissa hän osallistui matematiikan yhteiseen luomiseen. kirja "Homotopic Type Theory: Univalent Foundations of Mathematics ", jossa esitetään ohjelman tärkeimmät tulokset.
Journal of Functional Programming - ja Mathematical Structures in Computer Science -lehtien (molemmat Cambridge University Pressin julkaisija ) toimituskunnan jäsen. Springer-Verlagin ja Princeton University Pressin konstruktiivista algebraa ja todistusteoriaa koskevien kirjojen arvioija .
Palkinnot ja yhteisöt
Vuonna 2008 hän voitti merkittävän tutkimuspalkinnon Gödel Societylta ( englanniksi Kurt Gödel Society ) työstään metrisaatiotiloja ( englanniksi space of valuations ) [2] .
Vuonna 2011 hänet valittiin Royal Society of Sciences and Letters of Göteborg ( ruotsiksi: Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ) jäseneksi.
Tärkeimmät julkaisut
- Thierry Coquand. Girardin paradoksin analyysi (englanniksi) // Symposium on Logic in Computer Science (LIS'86), Cambridge, MA, 1986. - Cambridge, MA : IEEE , 1986. - P. 227-236 . — Burali-Forti-paradoksin analogin analyysi Martin-Löf-tyyppien intuitionistiselle teorialle.
- Thierry Coquand, Gerard Huet. Konstruktiolaskenta (englanti) // Information and Computation . - 1988. - Voi. 76 , nro. 2-3 . - s. 95-120 . — ISSN 0890-5401 . - doi : 10.1016/0890-5401(88)90005-3 . — rakennelaskentaa käsittelevä pääjulkaisu.
- Thierry Coquand. Klassisen logiikan todisteiden semantiikka (englanniksi) // Journal of Symbolic Logic . - 1995. - Voi. 60 , ei. 1 . - s. 325-337 . — ISSN 0022-4812 . - doi : 10.2307/2275524 . .
- Thierry Coquand. Sur un théorème de Kronecker careant les variétés algébriques (fr.) // Comptes rendus hebdomadaires des séances de l'Académie des sciences . - Paris, 2004. - Voi. 338 , nro 4 . _ — s. 291–294 . — ISSN 0001-4036 . - doi : 10.1016/j.crma.2003.12.008 .
- Heidän Coquand. Tyyppiteoria // Stanford Encyclopedia of Philosophy . - Stanford : Stanford University Publishing, 2010. - Artikkeli tyyppiteoriasta Stanford Encyclopedia of Philosophyssa .
Muistiinpanot
- ↑ Saksan kansalliskirjasto , Berliinin osavaltion kirjasto , Baijerin osavaltion kirjasto , Itävallan kansalliskirjaston tietue #122538900 // General Regulatory Control (GND) - 2012-2016.
- ↑ Åsa Ekvall. Thierry Coquand on saanut Kurt Gödel Centenary Research Prize -stipendin . Göteborgin yliopisto (6. huhtikuuta 2008). Haettu: 1. maaliskuuta 2014.
Linkit
- Thierry Cocanin kotisivu (englanniksi) . Haettu: 1. maaliskuuta 2014.
 Temaattiset sivustot | ||||
|---|---|---|---|---|
| ||||