Wednesday, October 10, 2018

Ada Lovelace Day 2018

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!


  1. I looked her up and noticed she didn't have a wikipedia page yet, so I made one for her: 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.

  2. Many thanks Sara! I checked that the wikipedia page on Coq ( has

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

  3. Also her main publication (as far as citations are concerned) is Inductive definitions in the system coq rules and properties
    C Paulin-Mohring
    International Conference on Typed Lambda Calculi and Applications, 328-345 (it has 588 citations as far as Scholar knows