Coq | |||
---|---|---|---|
Тип | Средство доказательства теорем | ||
Разработчики | INRIA; команда разработчиков | ||
Написана на | OCaml; C | ||
Операционная система | кроссплатформенность | ||
Первый выпуск | 1 мая 1989 года | ||
Аппаратная платформа | кроссплатформенное | ||
Последняя версия |
|
||
Репозиторий | github.com/coq/coq | ||
| |||
| |||
Состояние | активное | ||
Лицензия | LGPL 2.1 | ||
Сайт | coq.inria.fr | ||
Медиафайлы на Викискладе |
Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina)[2] с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.
Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal)[3], совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в Высшей нормальной школе Лиона.
Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана.