
Home Page: http://coq.inria.fr
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an IDE for semi-interactive development of machine-checked proofs. It is developed using the Objective Caml language (OCaml™ , with a bit of C. A complete reference manual, standard library, and other documents can be found on the Coq website. This is specialized software requiring a significant knowledge of formal mathematical theory, even if your intent is to develop or test software algorithms.