Интернет магазин китайских планшетных компьютеров

Компьютеры - Coq

В информатике Coq есть доказатель теорем, использующий собственный язык функционального программирования с зависимыми типами. Он позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели. Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.

Coq разработан во Франции в проекте TypiCal , совместно управляемом INRIA, Политехнической школой, Paris-Sud 11 University  и Национальным центром научных исследований. Ранее была группа и в École Normale Supérieure de Lyon .

Название «coq» на французском означает «петух». Оно следует французской традиции именовать исследовательские проекты названиями животных. Название также намекает на Thierry Coquand, который разработал исчисление конструкций вместе с Gérard Huet. Исчисление конструкций является теоретической базой Coq.