Christine Paulin-Mohring
Christine Paulin-Mohring, née le [1], est mathématicienne et informaticienne française. Elle développe l'assistant de preuve Coq.
| Naissance | |
|---|---|
| Nationalité | |
| Formation | |
| Activités |
| A travaillé pour |
ComUE Université Paris-Saclay (d) |
|---|---|
| Membre de | |
| Directeur de thèse | |
| Distinctions |
Biographie
Christine Paulin-Mohring obtient son doctorat en 1989 sous la direction de Gérard Huet[2]. Sa thèse portait sur l'extraction de programmes dans le Calcul des Constructions[3].
Après avoir été chargée de recherche au CNRS au laboratoire de l'informatique du parallélisme (LIP) de l'École normale supérieure de Lyon, elle est professeure à l'université Paris-Sud 11 depuis 1997[4]. Son mémoire d'habilitation à diriger les recherches portait sur les définitions inductives en théorie des types[5].
Entre 2012 et 2015, elle est coordinatrice scientifique du Labex DigiCosme[6]. Elle est actuellement membre du comité de rédaction du Journal of Formalized Reasoning[7].
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 qu'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[8].
Prix et distinctions
- prix Michel-Monpetit, Académie française des sciences, 2015[9].
- prix ACM SIGPLAN Programming Languages Software, pour le projet Coq, Association for Computing Machinery, 2013.
- prix ACM Software System, pour le projet Coq, Association for Computing Machinery, 2013[10].
Notes et références
- (BNF 12731197)
- Birth year from Library of Congress catalog entry, retrieved 2018-12-01.
- Thèse de Christine Paulin
- « bio », www.lri.fr (consulté le )
- HDR de Christine Paulin
- (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 )
- (en) « Christine Paulin-Mohring », sur awards.acm.org (consulté le )
Liens externes
- Ressources relatives Ă la recherche :