Georges Gonthier
Pour les articles homonymes, voir Gonthier.
Cet article est une ébauche concernant l’informatique.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
Georges Gonthier
| Naissance | |
|---|---|
| Nationalité | canadienne  |
| Activité | Informaticien |
| A travaillé pour | Microsoft Research |
|---|---|
| Directeur de thèse | |
| Site web | www.msr-inria.fr/researchers/georges-gonthier |
modifier - modifier le code - modifier Wikidata
Georges Gonthier est un chercheur canadien en informatique, effectuant sa recherche en Grande-Bretagne et en France. Ses domaines d'intérêt sont la conception des langages de programmation et leur sémantique, la théorie de la concurrence en programmation et son application à la sécurité, les méthodes et les outils pour la vérification formelle des programmes informatiques et des théories mathématiques. Il est notamment connu pour le développement complet, mécaniquement vérifié par ordinateur de la démonstration du théorème des quatre couleurs[1].
Travaux et distinctions
Georges Gonthier a entre autres travaillé[2] sur les langages concurrents et synchrones, en particulier le langage Esterel de Gérard Berry, sur la réduction du lambda-calcul avec Martín Abadi et Jean-Jacques Lévy, et sur la sécurité des communications de processus distribués avec Abadi et Cédric Fournet.
Ses recherches actuelles portent sur l'utilisation des assistants de preuve reposant sur la théorie des types, conçus et utilisés par des logiciens et des informaticiens, dans des domaines plus larges des mathématiques. En 2005, sa vérification automatique de la preuve[3] du théorème des quatre couleurs entièrement formalisée dans le système Coq a mis un terme[4] aux doutes de la communauté mathématique sur la validité des preuves automatisées de ce résultat[5]. Il dirige depuis le groupe Mathematical Components du centre commun Microsoft-INRIA qui travaille sur la formalisation de mathématiques plus fondamentales, dont la théorie des groupes finis.
Georges Gonthier reçoit le Grand Prix « Sciences de l'informatique » de la Fondation d'entreprise EADS en 2011[6].
Le , il annonce avoir terminé la formalisation en Coq de la preuve du théorème de Feit-Thompson, après 6 ans de travail avec son équipe[7]. Ce résultat permet d’affirmer la correction de la preuve de 250 pages écrite en 1963.
Article connexe
Liens externes
- Page de Georges Gonthier sur le site de l'École polytechnique
- Page de Georges Gonthier sur le site de Microsoft Research
- Page de l'équipe Mathematical Components sur le site de Microsoft Research
- Page de biographie du lauréat du prix « Sciences de l'informatique et leurs applications » sur le site de la Fondation d'entreprise EADS
Notes et références
- ↑ La Recherche, Société d'éditions scientifiques (Paris, France)
- ↑ Publications de Georges Gonthier (DPLB)
- ↑ "Formal Proof -- The Four-Color Theorem", par Georges Gonthier, dans les Notices of the American Mathematical Society
- ↑ "Last doubts removed about the proof of the Four Color Theorem", article de Keith Devlin pour la Mathematical Association of America, 2005
- ↑ article "Automated Reasoning" de la Stanford Encyclopedia of Philosophy
- ↑ Descriptif du Prix et zoom sur les travaux de recherche du lauréat
- ↑ G. Gonthier et al., « A Machine-Checked Proof of the Odd Order Theorem », HAL, Archives ouvertes, (lire en ligne)
Portail de l'informatique théorique 
Portail du Canada
