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

Serveur de réalisations aléatoires de modèles de questions éducatives préparées en un format html/LaTeX.

p5Visuel est un environnement de programmation visuelle destiné aux débutants.

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