Coq

Coq
Тип	Средство доказательства теорем
Разработчики	INRIA; команда разработчиков
Написана на	OCaml; C
Операционная система	кроссплатформенность
Первый выпуск	1 мая 1989 года
Аппаратная платформа	кроссплатформенное
Последняя версия	8.20.0 (3 сентября 2024)[1]
Репозиторий	github.com/coq/coq
Читаемые форматы файлов: Coq file format[вд]
Создаваемые форматы файлов: Coq file format[вд]
Состояние	активное
Лицензия	LGPL 2.1
Сайт	coq.inria.fr
Медиафайлы на Викискладе

Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina)^[2] с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.

Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal)^[3], совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в Высшей нормальной школе Лиона.

Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана.

1. ↑ Release Coq 8.20.0 — 2024.
2. ↑ Chlipala, 2013.
3. ↑ Архивированная копия  (неопр.). Дата обращения: 26 февраля 2009. Архивировано 26 февраля 2009 года.