Almost forgot about
Ada Lovelace Day again! The interwebs seem to be forgetting too. With all the bad
stuff happening in politics and all the accumulated work, caused by
(very nice, all the same!!) being Invited Speaker at the
Logic AI Summit in Luxembourg, no wonder.
Anyways, my hero figure this year is Professor
Christine Paulin-Mohring, Professor Université Paris-Sud and INRIA Saclay - Île-de-France.
Prof Paulin-Mohring is one of the people responsible for Coq,
the famous French theorem prover and an expert on automated theorem
proving using dependent type theory. I have not, so far, recognized any
of my heroes of Functional Programming, so this is about time, really.
Happy Ada Lovelace Day, Christine!
I looked her up and noticed she didn't have a wikipedia page yet, so I made one for her: https://en.wikipedia.org/wiki/Christine_Paulin-Mohring. If you have any other information on her and her work -- especially its significance and her publications (which aren't listed on her homepage as far as I could tell!), adding this info would help keep her page from being deleted for insignificance.
ReplyDeleteMany thanks Sara! I checked that the wikipedia page on Coq (https://en.wikipedia.org/wiki/Coq) has
ReplyDelete"The Association for Computing Machinery ACM rewarded Thierry Coquand, Gérard Pierre Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot and Pierre Castéran with the 2013 ACM Software System Award for Coq."
The also say [the name Coq is] also an indirect reference to Thierry Coquand who developed the Calculus of Constructions along with Gérard Pierre Huet and the Calculus of Inductive Constructions along with Christine Paulin-Mohring.
Also her main publication (as far as citations are concerned) is Inductive definitions in the system coq rules and properties
ReplyDeleteC Paulin-Mohring
International Conference on Typed Lambda Calculi and Applications, 328-345 (it has 588 citations as far as Scholar knows https://scholar.google.fr/citations?user=L-H2D9AAAAAJ&hl=en)