Cocan, Thierry

Thierry Coquand ( fr.  Thierry Coquand ; născut la 18 aprilie 1961 ) este un matematician francez , specialist în teoria tipurilor și demonstrarea automată , creator al calculului de construcție , co-organizator al programului de creare a bazelor univalente ale matematicii . Profesor la Facultatea de Informatică și Inginerie a Universității din Göteborg .

Biografie

Născut în Jalieu ( departamentul Isère ). În 1980 a absolvit Școala Normală Superioară din Paris , în 1982 a promovat „agregarea matematică” ( fr.  agrégation de mathématiques ) - concurs pentru dreptul de a preda matematica în licee. În 1985 şi-a susţinut teza de doctorat ( doctorat ) în informatică la INRIA sub îndrumarea lui Gerard Huet . În 1985-1989 a fost cercetător vizitator la INRIA, în 1989 a ocupat funcția de director de cercetare ( fr. directeur de recherche ).  

Din 1990 locuiește și lucrează în Suedia : a fost cercetător vizitator la Universitatea de Tehnologie Chalmers , iar din 1996 este profesor la Universitatea din Göteborg .

Lucrări științifice

În timp ce lucra cu Gérard Huet la mijlocul anilor 1980, el a dezvoltat calculul de construcție ,  un calcul λ polimorf de ordin superior cu tipuri dependente care ocupă cel mai înalt punct din cubul λ Barendregt și a devenit mai târziu baza software-ului de demonstrare automată Coq . sistem . (Numele „Coq” ascunde atât acronimul pentru calculul construcției, CoC , cât și prima parte a numelui de familie al lui Kokan.)

Publicații majore despre teoria tipurilor și demonstrarea automată. O serie de lucrări din anii 1990-2000 este dedicată topologiei inutile și algebrei constructive . 

Activitate organizatorica

Membru al comisiei de program al XIV-lea Congres Internațional de Logică, Metodologie și Filosofie (2011, Nancy ).

Împreună cu Vladimir Voevodsky și Steve Awodey , a coorganizat un program special de cercetare pentru anul universitar 2012-2013 la Institutul  de Studii Avansate , dedicat fundamentelor univalente ale matematicii , în cadrul acestuia participând la crearea comună a cartea „Teoria tipurilor homotopice: Fundamente univalente ale matematicii”, care prezintă principalele rezultate ale programului.

Membru al consiliilor editoriale ale revistelor Journal of Functional Programming și Mathematical Structures in Computer Science (ambele publicate de Cambridge University Press ). Revizor al cărților de algebră constructivă și teoria dovezilor pentru Springer-Verlag și Princeton University Press .

Premii și comunități

În 2008, a câștigat un premiu major de cercetare de la Societatea Gödel ( Societatea engleză  Kurt Gödel ) pentru munca sa privind spațiile de metrizări ( în engleză  spațiul evaluărilor ) [2] .

În 2011 a fost ales membru al Societății Regale de Științe și Litere din Göteborg ( suedeză: Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ).

Publicații majore

• Thierry Coquand. O analiză a paradoxului lui Girard  (engleză)  // Symposium on Logic in Computer Science (LIS'86), Cambridge, MA, 1986. - Cambridge, MA : IEEE , 1986. - P. 227-236 .  — analiza unui analog al paradoxului Burali-Forti pentru teoria intuiționistă a tipurilor Martin-Löf .
• Thierry Coquand, Gerard Huet. The calculus of constructions  (engleză)  // Information and Computation . - 1988. - Vol. 76 , nr. 2-3 . - P. 95-120 . — ISSN 0890-5401 . - doi : 10.1016/0890-5401(88)90005-3 .  — publicația principală despre calculul structurilor.
• Thierry Coquand. O semantică a dovezilor pentru logica clasică  (engleză)  // Journal of Symbolic Logic . - 1995. - Vol. 60 , nr. 1 . - P. 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 . _ — P. 291–294 . — ISSN 0001-4036 . - doi : 10.1016/j.crma.2003.12.008 .
• Theirry Coquand. Teoria tipurilor  // Stanford Encyclopedia of Philosophy . - Stanford : Stanford University Publishing, 2010.  - articol despre teoria tipurilor în Stanford Encyclopedia of Philosophy .

Note

1. ↑ Biblioteca Națională Germană , Biblioteca de stat din Berlin , Biblioteca de stat bavareza , Înregistrarea Bibliotecii Naționale din Austria #122538900 // Controlul general de reglementare (GND) - 2012-2016.
2. ↑ Åsa Ekvall. Thierry Coquand a primit bursa Kurt Gödel Centenar Research  Prize . Universitatea din Göteborg (6 aprilie 2008). Preluat: 1 martie 2014.

Link -uri

• Pagina de pornire a lui Thierry Cocan  (engleză) . Preluat: 1 martie 2014.

Site-uri tematice	Genealogie matematică ResearchGate zbMATH Deschide
În cataloagele bibliografice GND : 122538900 ISNI : 0000 0000 8328 1119 J9U : 987007452171305171 LCCN : n00016832 NTA : 213085054 SUDOC : 139931422 VIAF : 117236995 World Cat VIAF : 117236995