Cocan, Thierry
| Thierry Cocan | |
|---|---|
| Thierry Coquand | |
| Födelsedatum | 18 april 1961 [1] (61 år) |
| Födelseort | Jalieu (Frankrike, departementet Isère) |
| Land | Frankrike |
| Vetenskaplig sfär | Grunderna för matematik , teoretisk datavetenskap |
| Arbetsplats | Göteborgs universitet |
| Alma mater | Higher Normal School (Paris) |
| Akademisk examen | PhD |
| Akademisk titel | Professor |
| vetenskaplig rådgivare | Gerard Huet |
| Känd som | Utvecklare av konstruktionskalkyl, medarrangör av programmet för univalenta grunder för matematik, forskare av meningslös topologi |
| Utmärkelser och priser | Gödel Society Research Prize (2008) |
| Mediafiler på Wikimedia Commons | |
Thierry Coquand ( fr. Thierry Coquand ; född 18 april 1961 ) är en fransk matematiker , specialist på typteori och automatiskt bevis , skapare av konstruktionskalkylen , medarrangör av programmet för att skapa univalenta grunder för matematik . Professor vid fakulteten för informatik och teknik vid Göteborgs universitet .
Biografi
Född i Jalieu ( departementet Isère ). 1980 tog han examen från Higher Normal School i Paris , 1982 klarade han den "matematiska aggregation" ( fr. agrégation de mathématiques ) - ett konkurrenskraftigt prov för rätten att undervisa i matematik i gymnasieskolor. 1985 disputerade han på sin doktorsavhandling ( PhD ) i datavetenskap vid INRIA under ledning av Gerard Huet . 1985-1989 var han gästforskare vid INRIA, 1989 tjänstgjorde han som forskningschef ( fr. directeur de recherche ).
Sedan 1990 har han bott och arbetat i Sverige : han var gästforskare vid Chalmers tekniska högskola och sedan 1996 är han professor vid Göteborgs universitet .
Vetenskapliga arbeten
När han arbetade med Gérard Huet i mitten av 1980-talet utvecklade han konstruktionskalkylen , en högre ordningens polymorf λ-kalkyl med beroende typer som upptar den högsta punkten i Barendregt λ-kuben och som senare blev grunden för Coqs automatiska bevisprogram. system . (Namnet "Coq" döljer både akronymen för konstruktionskalkyl, CoC , och den första delen av Kokans efternamn.)
Större publikationer om typteori och automatiskt bevis. En serie verk från 1990-2000-talet ägnas åt meningslös topologi och konstruktiv algebra .
Organisationsaktivitet
Medlem av programkommittén för XIV International Congress on Logic, Methodology and Philosophy (2011, Nancy ).
Tillsammans med Vladimir Voevodsky och Steve Awodey organiserade han ett speciellt forskningsprogram för läsåret 2012-2013 vid Institutet för avancerade studier , tillägnat matematikens univalenta grunder , inom dess ram deltog han i det gemensamma skapandet av boken "Homotopic Type Theory: Univalent Foundations of Mathematics", som beskriver programmets huvudresultat.
Ledamot i redaktionen för tidskrifterna Journal of Functional Programming och Mathematical Structures in Computer Science (båda publicerade av Cambridge University Press ). Recensent av böcker om konstruktiv algebra och bevisteori för Springer-Verlag och Princeton University Press .
Utmärkelser och gemenskaper
2008 vann han ett stort forskningspris från Gödel Society ( English Kurt Gödel Society ) för sitt arbete med spaces of metrizations ( English space of valuations ) [2] .
2011 valdes han till medlem av Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ( svenska: Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ).
Stora publikationer
- Thierry Coquand. En analys av Girards paradox (engelska) // Symposium on Logic in Computer Science (LIS'86), Cambridge, MA, 1986. - Cambridge, MA : IEEE , 1986. - S. 227-236 . — Analys av en analog till Burali-Forti-paradoxen för Martin-Löf-typers intuitionistiska teori .
- Thierry Coquand, Gerard Huet. Konstruktionskalkylen (engelska) // Information and Computation . - 1988. - Vol. 76 , nr. 2-3 . - S. 95-120 . — ISSN 0890-5401 . - doi : 10.1016/0890-5401(88)90005-3 . — Huvudpublikationen om beräkning av strukturer.
- Thierry Coquand. En semantik av bevis för klassisk logik (engelska) // Journal of Symbolic Logic . - 1995. - Vol. 60 , nej. 1 . - s. 325-337 . — ISSN 0022-4812 . - doi : 10.2307/2275524 . .
- Thierry Coquand. Sur un théorème de Kronecker concernant les variétés algébriques (fr.) // Comptes rendus hebdomadaires des séances de l'Académie des sciences . - Paris, 2004. - Vol. 338 , nr 4 . _ — S. 291–294 . — ISSN 0001-4036 . - doi : 10.1016/j.crma.2003.12.008 .
- Deras Coquand. Typteori // Stanford Encyclopedia of Philosophy . - Stanford : Stanford University Publishing, 2010. - Artikel om typteori i Stanford Encyclopedia of Philosophy .
Anteckningar
- ↑ Tyska nationalbiblioteket , Berlins statsbibliotek , Bayerns statsbibliotek , österrikiska nationalbibliotekets register #122538900 // General Regulatory Control (GND) - 2012-2016.
- ↑ Åsa Ekvall. Thierry Coquand har tilldelats Kurt Gödel Centenary Research Prize Fellowship . Göteborgs universitet (6 april 2008). Hämtad: 1 mars 2014.
Länkar
- Hemsida för Thierry Cocan (engelska) . Hämtad: 1 mars 2014.
 Tematiska platser | ||||
|---|---|---|---|---|
| ||||