Utilisatrice:DeuxPlusQuatre/Christine Paulin-Mohring
Christine Paulin-Mohring née en 1962 est mathématicienne et informaticienne française. Elle développe l'assistant de preuve Coq.
Biographie
modifierChristine Paulin-Mohring obtient son doctorat en 1989 sous la direction de Gérard Huet[1]. Elle est professeure à l'Université Paris-Sud 11 depuis 1997[2].
Entre 2012 et 2015, elle est coordinatrice scientifique du Labex DigiCosme[3]. Elle est actuellement membre du comité de rédaction du Journal of Formalized Reasoning[4].
Elle travaille avec Gérard Huet et Thierry Coquand sur un démonstrateur interactif de théorèmes à l’Inria. Il s'agit du logicel Coq, un assistant de preuve. Thierry Coquand et Gérard Huet conçoivent la logique du logiciel et le calcul des constructions. Christine Paulin-Mohring implémente une nouvelle construction : les types inductifs et un mécanisme d’extraction qui permet d’obtenir automatiquement un programme zéro défaut à partir d’une preuve. Cela permet de vérifier des calculs majeurs en mathématiques. Par exemple, Georges Gonthier et son équipe ont validé le théorème des quatre couleurs, qui dit que toute carte peut être coloriée avec quatre couleurs uniquement, en assurant que deux régions contigües reçoivent toujours deux couleurs distinctes. L'apport de Christine Paulin-Mohring est que une preuve vérifiée par le logiciel Coq peut être convertie en un programme zéro défaut, c'est-à-dire sans bug, conforme aux spécifications. L’impact du logiciel Coq sur la communauté scientifique est très important[5].
Prix et distinctions
modifier- prix Michel-Monpetit, Académie française des sciences, 2015[6].
- prix ACM Software System, pour le projet Coq, Association for Computing Machinery, 2013.
Notes et références
modifier- Birth year from Library of Congress catalog entry, retrieved 2018-12-01.
- « bio », www.lri.fr (consulté le )
- (en) « Labex DigiCosme | Organisation-EN », digicosme.lri.fr (consulté le )
- (en-US) « Editorial Team », jfr.unibo.it (consulté le )
- binaire, « Christine Paulin et les Logiciels Zéro Défaut », sur binaire, (consulté le )
- « Lauréats 2015 des prix thématiques », French Academy of Sciences (consulté le )
[[Catégorie:Naissance en 1962]] [[Catégorie:Informaticien français]] [[Catégorie:Mathématicien français]] [[Catégorie:Mathématicien du XXe siècle]] [[Catégorie:Mathématicien du XXIe siècle]] [[Catégorie:Personnalité en logique mathématique]]