Thierry Coquand

Thierry Coquand (; born 18 April 1961) is a French computer scientist and mathematician who is since 1996 a professor of computer science at the University of Gothenburg, having formerly worked at INRIA. He is known for his work in constructive mathematics, especially the calculus of constructions.

He received his Ph.D. under the supervision of Gérard Huet, another academic who has experience in both mathematics and computer science. 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". Coquand and Huet published another joint article in September of that year which further expanded on their ideas regarding constructive mathematics. In the following year, 1986, Coquand published a noteworthy paper about Girard's paradox in the System U logic system. Since then, Coquand has written a wide variety of papers in both French and English.

In addition to his contributions to theoretical computer science, Coquand is also known as the co-creator of the Rocq (formerly named Coq, the name is a reference partly to Coquand's surname) proof assistant, which he began developing in 1984 while working at INRIA (a French national research institute for computer science and mathematics), and which was released officially in 1989. Coq won the Association for Computing Machinery (ACM) SIGPLAN Programming Languages Software Award in 2013, for "provid[ing] a rich environment for interactive development of machine-checked formal reasoning". Rocq has been used to provide novel solutions for mathematical problems, especially for those that have a non-surveyable proof, such as the four color theorem. It has also been used in software development, such as with the CompCert C compiler.

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.