Cocan, Thierry

Thierry Coquand ( fr.  Thierry Coquand ; født 18. april, 1961 ) er en fransk matematiker , specialist i typeteori og automatisk bevisførelse , skaber af konstruktionsregningen , medarrangør af programmet til at skabe univalent grundlag for matematik . Professor ved fakultetet for informatik og teknik ved Göteborgs Universitet .

Biografi

Født i Jalieu ( afdelingen af ​​Isère ). I 1980 dimitterede han fra Higher Normal School i Paris , i 1982 bestod han "matematisk sammenlægning" ( fr.  agrégation de mathématiques ) - en konkurrencepræget eksamen for retten til at undervise i matematik på gymnasier. I 1985 forsvarede han sin doktorafhandling ( ph.d. ) i datalogi ved INRIA under vejledning af Gerard Huet . I 1985-1989 var han gæsteforsker ved INRIA, i 1989 fungerede han som forskningsdirektør ( fr. directeur de recherche ).  

Siden 1990 har han boet og arbejdet i Sverige : han var gæsteforsker ved Chalmers Tekniske Universitet , og siden 1996 har han været professor ved Göteborgs Universitet .

Videnskabelige værker

Mens han arbejdede med Gérard Huet i midten af ​​1980'erne, udviklede han konstruktionskalkylen ,  en højere ordens polymorf λ-regning med afhængige typer , der indtager det højeste punkt i Barendregt λ-terningen og senere blev grundlaget for Coqs automatiske bevissoftware system . (Navnet "Coq" skjuler både akronymet for konstruktionsregning, CoC , og den første del af Kokans efternavn.)

Større publikationer om typeteori og automatisk bevisførelse. En række værker fra 1990'erne-2000'erne er viet til meningsløs topologi og konstruktiv algebra . 

Organisatorisk aktivitet

Medlem af programudvalget for XIV International Congress on Logic, Methodology and Philosophy (2011, Nancy ).

Sammen med Vladimir Voevodsky og Steve Awodey var han med til at organisere et særligt forskningsprogram for det akademiske år 2012-2013 ved Institute  for Advanced Study , dedikeret til matematikkens univalente grundlag , inden for dets rammer deltog han i den fælles oprettelse af bog "Homotopic Type Theory: Univalent Foundations of Mathematics", som skitserer de vigtigste resultater af programmet.

Medlem af redaktionen for tidsskrifterne Journal of Functional Programming og Mathematical Structures in Computer Science (begge udgivet af Cambridge University Press ). Anmelder af bøger om konstruktiv algebra og bevisteori for Springer-Verlag og Princeton University Press .

Priser og fællesskaber

I 2008 vandt han en stor forskningspris fra Gödel Society ( English  Kurt Gödel Society ) for sit arbejde med spaces of metrizations ( English  space of valuations ) [2] .

I 2011 blev han valgt til medlem af Royal Society of Sciences and Letters of Gothenburg ( svensk: Kungliga Vetenskaps- och Vitterhetssamhället i Göteborg ).

Større publikationer

• Thierry Coquand. En analyse af Girards paradoks  (engelsk)  // Symposium on Logic in Computer Science (LIS'86), Cambridge, MA, 1986. - Cambridge, MA : IEEE , 1986. - S. 227-236 .  — analyse af en analog af Burali-Forti-paradokset for Martin-Löf-typernes intuitionistiske teori .
• Thierry Coquand, Gerard Huet. The calculus of constructions  (engelsk)  // Information and Computation . - 1988. - Bd. 76 , nr. 2-3 . - S. 95-120 . — ISSN 0890-5401 . - doi : 10.1016/0890-5401(88)90005-3 .  — hovedpublikationen om beregning af strukturer.
• Thierry Coquand. En semantik af evidens for klassisk logik  (engelsk)  // Journal of Symbolic Logic . - 1995. - Bd. 60 , nr. 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. - Bd. 338 , nr . 4 . — S. 291–294 . — ISSN 0001-4036 . - doi : 10.1016/j.crma.2003.12.008 .
• Deres Coquand. Typeteori  // Stanford Encyclopedia of Philosophy . - Stanford : Stanford University Publishing, 2010.  - artikel om typeteori i Stanford Encyclopedia of Philosophy .

Noter

1. ↑ German National Library , Berlin Statsbibliotek , Bayerske Statsbibliotek , Austrian National Library Record #122538900 // General Regulatory Control (GND) - 2012-2016.
2. ↑ Åsa Ekvall. Thierry Coquand er blevet tildelt Kurt Gödel Centenary Research Prize  Fellowship . Göteborgs Universitet (6. april 2008). Hentet: 1. marts 2014.

Links

• Hjemmeside for Thierry Cocan  (engelsk) . Hentet: 1. marts 2014.

Tematiske steder	Matematisk genealogi ResearchGate zbMATH Åbn
I bibliografiske kataloger GND : 122538900 ISNI : 0000 0000 8328 1119 J9U : 987007452171305171 LCCN : n00016832 NTA : 213085054 SUDOC : 139931422 VIAF : 117236995 World Cat VIAF : 117236995