Thierry Coquand

Thierry Coquand is a French logician and computer scientist whose work has reshaped the foundations of constructive mathematics and dependently typed programming. He co-created the Coq proof assistant with Gérard Huet in 1984, giving the world one of the first practical systems in which mathematical proofs and computer programs were the same kind of object. He later developed Cubical Type Theory with Marc Bezem and Simon Huber, providing a constructive account of univalence and higher-dimensional equality that does not require the univalent axiom itself — a move that turned homotopy type theory from a philosophical program into a computational one.

Coquand's intellectual trajectory is a single sustained argument: that mathematics is computation, that proofs are programs, and that the separation of logic from programming language design is a historical accident that formal methods are finally correcting. The systems he has built — Coq, Agda's foundations, and the cubical model — are not tools but demonstrations of this thesis in action.