Christine Paulin-Mohring (born 1962)[1] is a mathematical logician and computer scientist, and Professor Faculté des Sciences at Paris-Saclay University,[2] best known for developing the interactive theorem prover Coq.
Paulin-Mohring received her PhD in 1989 under the supervision of Gérard Huet.
she is a member of the editorial board of the Journal of Formalized Reasoning.
[6] Paulin-Mohring won the Michel-Monpetit Prize [fr] of the French Academy of Sciences in 2015.
[7] She and the rest of the Coq development team (Thierry Coquand, Gérard Huet, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot and Pierre Castéran) won the 2013 ACM Software System Award[8][9] awarded by the Association for Computing Machinery.