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

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

Autres suggestions...

4

Obtenir de grandes feuilles de calcul pour soroban sur ordinateur ou des petites sur tablette ou smartphone.

5

SageMath est un logiciel libre de calcul mathématique.

2

Giac/Xcas est un système de calcul formel libre pour Windows, Mac OSX et Linux/Unix (licence GPL3)