Le logiciel Coq est un assistant à la preuve formelle développé à l’Inria. Il est fondé sur le Calcul des Constructions de Thierry Coquand, une théorie des types d’ordre supérieur, et exploite largement la correspondance de Curry-Howard. Coq peut manipuler des énoncés du calcul et permet de faire une vérification mécaniques de ces énoncés. Il peut aussi aider à la recherche de preuves formelles d’énoncés mathématiques (par exemple, le théorème des quatre couleurs) ainsi que à la vérification formelle de programmes informatiques (par exemple, le compilateur CompCert C).