Après des études à l'École normale supérieure de Paris, Thierry Coquand passe sa thèse d'informatique théorique en 1985, introduisant la théorie des constructions, formalisme utilisé dans plusieurs systèmes d'assistants à la démonstration. Depuis 1996, il est professeur en informatique à l'université de Göteborg, en Suède. Ses recherches concernent les mathématiques constructives, la théorie des types et ses applications pour la représentation des preuves sur ordinateur, et la sémantique des langages de programmation. Il a été coorganisateur, avec Vladimir Voevodsky et Steve Awodey, de l'année spéciale 2012-2013 à l’Institute of Advanced Study, Princeton, sur les Univalent Foundations of Mathematics. Ses travaux récents ont pour but de donner un sens effectif à l'axiome d'univalence, introduit par Voevodsky, et aux modèles de faisceaux (topos d'ordre supérieur). Pour ses travaux en logique, il a eu le Kurt Godel Centenary Research Prize 2008, et pour ses travaux sur les assistants de preuve, il a reçu, en collaboration, le ACM SIGPLAN Programming Languages Software Award, 2013.