Thierry Coquand (; born 18 April 1961) is a French computer scientist and mathematician who is currently a professor of

computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

at the

University of Gothenburg The University of Gothenburg () is a List of universities in Sweden, university in Sweden's second largest city, Gothenburg. Founded in 1891, the university is the third-oldest of the current List of universities in Sweden#Public universities, S ...

, having previously worked at

INRIA The National Institute for Research in Digital Science and Technology (Inria) () is a French national research institution focusing on computer science and applied mathematics. It was created under the name French Institute for Research in Comp ...

. He is known for his work in

constructive mathematics In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...

, especially the

calculus of constructions In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reaso ...

. He received his Ph.D. under the supervision of

Gérard Huet Gérard Pierre Huet (; born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and ...

, 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 for being the co-creator of the Rocq (previously known as ''Coq'', this name partially being a reference to Coquand's surname)

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof edi ...

, 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. Coq won the ACM SIGPLAN Programming Languages Software Award in 2013, for "provid nga 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 In mathematics, the four color theorem, or the four color map theorem, states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. ''Adjacent'' means that two regions shar ...

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

References

External links

* , Chalmers * {{DEFAULTSORT:Coquand, Thierry French computer scientists École Normale Supérieure alumni 20th-century French mathematicians 21st-century French mathematicians Academic staff of the University of Gothenburg 1961 births Living people

See also

References

External links