
Sito web: http://coq.inria.fr
Coq č un sistema di gestione di dimostrazioni. Fornisce un linguaggio formale per la scrittura di definizioni matematiche, algoritmi eseguibili e teoremi, insieme con un IDE per sviluppo semi-interattivo di dimostrazioni verificate automaticamente. Č sviluppato utilizzando Objective Caml e Camlp5. Nel sito web di Coq si trovano un manuale di riferimento, una libreria standard e altri documenti. Questo software č specialistico e richiede notevoli conoscenze sulle teorie di matematica formale, anche se il vostro scopo č sviluppare o provare algoritmi software.