| Születés |
1962. április 18 Montreal |
|---|---|
| Állampolgárság | kanadai |
| Tevékenység | Informatikus |
| Dolgozott valakinek | Microsoft Research |
|---|---|
| Területek | Számítástechnika , matematikai logika |
| Weboldal | www.msr-inria.fr/researchers/georges-gonthier |
Georges Gonthier egy kanadai kutató a számítástechnikában, elvégzése a kutatást a Nagy-Britannia és Franciaország . Érdeklődési területe a programozási nyelvek és szemantikájuk megtervezése, a versenyképes elmélet a programozásban és alkalmazásában a biztonságban, a számítógépes programok és a matematikai elméletek formális ellenőrzésének módszerei és eszközei. Elsősorban arról ismert, hogy a négy színű tétel bemutatását teljes egészében számítógépes fejlesztéssel ellenőrzik .
Georges Gonthier többek között dolgozott a versenytársak és a szinkron nyelvek, különösen a nyelvi Esterel a Gérard Berry , csökkentésére lambda-kalkulus az Martín Abádi és Jean-Jacques Levy , és folyamat biztonság kommunikációs eloszlású Abádi és Cedric Fournet .
Jelenlegi kutatása a logikusok és az informatikusok által tervezett és használt típuselméleten alapuló igazoló asszisztensek használatára összpontosít a matematika tágabb területein. 2005 - ben a Coq rendszerben teljesen formalizált négyszínű tétel igazolásának automatikus ellenőrzése véget vetett a matematikai közösség kételyeinek az eredmény automatizált bizonyításainak érvényességével kapcsolatban. A Matematikai összetevők csoportból a Microsoft - INRIA közös központot vezeti, amely az alapvetőbb matematika, ezen belül a véges csoportelmélet formalizálásán dolgozik .
Georges Gonthier kapta meg a „Computer Science” nagydíjat az EADS Corporate Alapítvány a 2011 .
A 2012. szeptember 20, bejelentette, hogy a csapatával végzett 6 éves munka után Coq-ban formalizálta a Feit-Thompson tétel igazolását . Ez az eredmény megerősíti az 1963-ban írt 250 oldalas igazolás helyességét.