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