Thierry Coquand
Thierry Coquand ( franska: [kɔkɑ̃] ; född 18 april 1961 i Bourgoin-Jallieu , Isère , Frankrike) är en fransk datavetare och matematiker som för närvarande är professor i datavetenskap vid Göteborgs universitet , efter att ha tidigare arbetat vid INRIA . Han är känd för sitt arbete inom konstruktiv matematik , särskilt kalkylen för konstruktioner .
Han fick sin Ph.D. under överinseende av Gérard Huet , en annan akademiker som har erfarenhet av både matematik och datavetenskap. Enligt ACM Digital Library var hans första publicerade artikel ett samarbete från 1985 med Huet med titeln "Constructions: A Higher Order Proof System for Mechanizing Mathematics". Coquand och Huet publicerade en annan gemensam artikel i september samma år som ytterligare utökade sina idéer om konstruktiv matematik. Året därpå, 1986, publicerade Coquand en anmärkningsvärd artikel om Girards paradox i System U-logiksystemet. Sedan dess har Coquand skrivit en mängd olika uppsatser på både franska och engelska.
Förutom sina bidrag till teoretisk datavetenskap är Coquand också känd för att vara medskaparen av Coq ( namnet är delvis en referens till Coquands efternamn) bevisassistent, som han började utveckla 1984 medan han arbetade på INRIA (en franska nationella forskningsinstitutet för datavetenskap och matematik), och som släpptes officiellt 1989. Coq vann ACM SIGPLAN Programming Languages Software Award 2013, för att "tillhandahålla en rik miljö för interaktiv utveckling av maskinkontrollerade formella resonemang" . Coq har använts för att tillhandahålla nya lösningar för matematiska problem, särskilt för de som har ett icke-mätbart bevis, som fyrafärgssatsen . Den har också använts i mjukvaruutveckling, som med CompCert C -kompilatorn.
Coquand håller ofta föredrag om de ämnen som han är specialiserad på, till exempel hans beskrivning av professorn Thorsten Altenkirch vid University of Nottingham .
Se även
externa länkar
- Akademisk hemsida
- Thierry Coquand på DBLP Bibliography Server