Thierry Coquand

According to the ACM Digital Library, his first published article was a 1985 collaboration with Huet titled "Constructions: A Higher Order Proof System for Mechanizing Mathematics".

[2] Coquand and Huet published another joint article in September of that year which further expanded on their ideas regarding constructive mathematics.

In addition to his contributions to theoretical computer science, Coquand is also known for being the co-creator of the Coq (the name partially being a reference to Coquand's surname) proof assistant, which he began development of in 1984 while working at INRIA (a French national research institute for computer science and mathematics), and which was officially released in 1989.

[5] Coq won the ACM SIGPLAN Programming Languages Software Award in 2013, for "provid[ing] a rich environment for interactive development of machine-checked formal reasoning".

[8] Coquand often gives talks about the subjects that he specializes in, such as his description of the work of University of Nottingham professor Thorsten Altenkirch.