Thierry Coquand

Thierry Coquand (born April 18, 1961) is a French computer scientist and mathematician who has been a professor of computer science at the University of Gothenburg since 1996, after earlier work at INRIA, the French national research institute. His work centers on type theory and constructive mathematics, particularly the calculus of constructions. He co-created the proof assistant now called Rocq, formerly named Coq after his own surname, beginning development in 1984 and officially releasing it in 1989; the software received the ACM SIGPLAN Programming Languages Software Award in 2013 and has been applied to problems including the four color theorem and the CompCert verified C compiler. He earned his PhD under the supervision of Gerard Huet, with whom he co-authored his first published article in 1985, Constructions: A Higher Order Proof System for Mechanizing Mathematics.