Thierry Coquand is a French computer scientist and logician. He was born on September 24, 1957, in Lyon, France. Coquand is known for his contributions to type theory, formal semantics, and constructive mathematics. Under the supervision of [[Gérard Huet]], Coquand obtained his Ph.D. in Computer Science from the University of Aix-Marseille in 1983. Coquand has held various academic positions throughout his career. Currently, he is a professor of computer science at the University of Gothenburg in Sweden. Coquand's research interests lie primarily in the field of type theory and its applications. He has made significant contributions to the development of constructive type theories, which are mathematical formalisms that emphasize computation and constructive proofs. His work has helped bridge the gap between logic and computer science by providing a foundation for programming languages with strong typing systems. In addition to his work on [[type theory]], Coquand has also made contributions to other areas of computer science such as programming language design and formal verification. He has published numerous papers on topics including proof theory, category theory, lambda calculus, and homotopy type theory. Overall, Thierry Coquand is a prominent figure in the field of computer science and logic. His work has had a significant impact on type theory and its applications in programming languages and formal verification. # References ```dataview Table title as Title, authors as Authors where contains(authors, "Thierry Coquand") ```