L'assistant de preuve Coq propose un environnement sophistiqué pour le développement de preuves mathématiques vérifiées par ordinateur. La preuve du théorème des quatre couleurs, du théorème de Feit-Thomson (classification des groupes finis) ou encore le développement d'un compilateur C optimisant complètement prouvé sont des exemples emblématiques des possibilités de Coq. Le langage sous-jacent à cet outil (le calcul des constructions) a été proposé par Coquand et Huet en 84 puis étendu par Coquand et Paulin. Le système Coq a été développé activement depuis cette époque avec de nombreuses versions successives et la contribution de plus de 30 personnes. Le développement a été coordonné par Gérard Huet puis par Christine Paulin (de 1996 à 2002) et actuellement par Hugo Herbelin.