Thierry Coquand

计算机科学家，Rocq（原 Coq）交互式定理证明器的创始者之一。1984年在法国国家信息与自动化研究院（INRIA-Rocquencourt）基于构造演算（Calculus of Constructions）的实现启动了该项目，与 Gérard Huet 共同奠定了 Rocq/Coq 的基础。