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.
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!