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].
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 logiciel 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 contiguës 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].
