Thierry Coquand

After studying at the École normale supérieure in Paris, Thierry Coquand obtained his PhD in theoretical computer science in 1985, introducing construction theory, a formalism used in several proof assistant systems. Since 1996, he has been Professor of Computer Science at the University of Gothenburg, Sweden. His research interests include constructive mathematics, type theory and its applications to proof representation on computers, and the semantics of programming languages. He was co-organizer, with Vladimir Voevodsky and Steve Awodey, of the 2012-2013 special year at theInstitute of Advanced Study, Princeton, on Univalent Foundations of Mathematics. His recent work aims to give effective meaning to the univalence axiom, introduced by Voevoedsky, and to beam models (higher-order topos). For this work in logic, he was awarded the Kurt Godel Centenary Research Prize 2008, and for his work on proof assistants, he received, in collaboration, the ACM SIGPLAN Programming Languages Software Award, 2013.