Thierry Coquand (French:[kɔkɑ̃]; born 18 April 1961) is a French computer scientist and mathematician who is currently a professor of computer science at the University of Gothenburg,[1] having previously 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".[2] Coquand and Huet published another joint article in September of that year which further expanded on their ideas regarding constructive mathematics.[3] In the following year, 1986, Coquand published a noteworthy paper about Girard's paradox in the System U logic system.[4] 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 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".[6][7] Coq 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.[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.[9]
^"Thierry Coquand". University of Gothenburg. Archived from the original on 27 March 2023. Retrieved 27 March 2023.
^Constructions: A Higher Order Proof System for Mechanizing Mathematics. April 1985. pp. 151–184. ISBN 9783540159834. Archived from the original on 24 February 2023. Retrieved 24 February 2023.
^Coquand, Thierry; Huet, Gérard (1985). "A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction". Journal of Symbolic Computation. 1 (3): 323–328. doi:10.1016/S0747-7171(85)80040-7. Archived from the original on 24 February 2023. Retrieved 24 February 2023.
^"An analysis of Girard's paradox". Archived from the original on 24 February 2023. Retrieved 24 February 2023.
^"What is Coq?". Archived from the original on 24 February 2023. Retrieved 24 February 2023.
^"Coq received ACM SIGPLAN Programming Languages Software 2013 award". Archived from the original on 22 February 2023. Retrieved 22 February 2023.
^"Programming Languages Software Award". Archived from the original on 25 February 2023. Retrieved 25 February 2023.
^"Thierry Coquand". Archived from the original on 25 February 2023. Retrieved 25 February 2023.
^"Paradoxes and Definitions" (PDF). Archived (PDF) from the original on 25 February 2023. Retrieved 25 February 2023.
ThierryCoquand (French: [kɔkɑ̃]; born 18 April 1961) is a French computer scientist and mathematician who is currently a professor of computer science...
Coquand is a French surname. Notable people with the surname include: Henri Coquand (1813–1881), French geologist and paleontologist ThierryCoquand (born...
science, the calculus of constructions (CoC) is a type theory created by ThierryCoquand. It can serve as both a typed programming language and as constructive...
milestone for univalent foundations was the Bourbaki Seminar talk by ThierryCoquand in June 2014. Univalent foundations originated from certain attempts...
and mathematical logic. The program was organized by Steve Awodey, ThierryCoquand and Vladimir Voevodsky. During the program Peter Aczel, who was one...
proof-writing systems use a type theory for their foundation. A common one is ThierryCoquand's Calculus of Inductive Constructions. Type theory was created to avoid...
logical systems as Per Martin-Löf's intuitionistic type theory, and ThierryCoquand and Gérard Huet's calculus of constructions. Until the end of 19th...
and judgments becomes the standard for presenting future theories. ThierryCoquand and Gérard Huet created the Calculus of Constructions, a dependent...
(1591–1606) S. Barry Cooper (UK, 1943–2015) Jack Copeland (UK, born 1950) ThierryCoquand (France, born 1961) John Corcoran (US, 1937–2021) Newton da Costa (Brazil...
theory of foundations. The program was organized by Steve Awodey, ThierryCoquand and Vladimir Voevodsky, and resulted in a book being published in homotopy...
Richard Stallman 2014 Mach Richard Rashid, Avie Tevanian 2013 Coq ThierryCoquand, Gérard Pierre Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe...
of mathematics, has the advantage of being simpler in structure." ThierryCoquand (20 January 2010). "Type Theory". Stanford Encyclopedia of Philosophy...
programming languages, compilers, optimization, and static analysis ThierryCoquand, ACM SIGPLAN 2013 PL Software Award and the 2015 ACM Software System...
Global Information