Browsing Slovenian translation

40.

<application>Coq</application> 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 Objective Caml and Camlp5. A complete reference manual, standard library and other documents are found on it 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.