Onglets principaux

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).

Tags: 
Disponible sur: 
Version: 
Logiciel en version stable (publié)
Langue: 
Créateur(s): 
Thierry Coquand
Société ou organisation: 
Inria

Autres suggestions...

Le Frido contient des mathématiques du niveau de l’agrégation.

Pour s'entraîner aux additions, soustractions, multiplications et divisions en jouant.

MuPhyN - Multi Physical Nexus - est un logiciel de simula