Coq - это интерактивное средство доказательства теорем, впервые выпущенное в 1989 году. Оно позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации . Coq работает в рамках теории исчисления индуктивных построений , производной от исчисления построений . Coq не является автоматическим средством доказательства теорем, но включает в себя тактику ( процедуры ) автоматического доказательства теорем и различные процедуры принятия решений .
Разработчики) | Команда разработчиков Coq |
---|---|
Первый выпуск | 1 мая 1989 г . | (версия 4.10)
Стабильный выпуск | 8.13.0 [1] / 7 января 2021 г . |
Предварительный выпуск | 8.13 + beta1 [2] / 7 декабря 2020 г . |
Репозиторий | github |
Написано в | OCaml |
Операционная система | Кроссплатформенность |
Доступно в | английский |
Тип | Помощник доказательства |
Лицензия | LGPLv2.1 |
Веб-сайт | coq |
Ассоциация вычислительной техники награждена Тьерри Кокана , Gérard HUET , Кристин Паулина-Möhring , Бруно Баррас, Жан-Кристоф Filliâtre Уго Herbelin, Четан Мурти, Ив Берто, и Пьер Castéran с 2013 годом премией ACM Software System для Coq.
Coq назван в честь главного разработчика Тьерри Коквана. [ необходима цитата ]
Обзор
Если рассматривать его как язык программирования, Coq реализует функциональный язык программирования с зависимой типизацией ; [3], если рассматривать ее как логическую систему, она реализует теорию типов более высокого порядка . Разработка Coq с 1984 года поддерживается INRIA , в настоящее время в сотрудничестве с École Polytechnique , Университетом Париж-Юг , Парижским университетом Дидро и CNRS . В 1990-х годах ENS Lyon также был частью проекта. Разработка Coq была инициирована Жераром Юэ и Тьерри Кокваном, и с момента ее создания более 40 человек, в основном исследователи, внесли свои функции в основную систему. Группу внедрения последовательно координировали Жерар Юэ, Кристин Полин-Моринг, Хьюго Эрбелен и Матье Созо. Coq в основном реализуется в OCaml с небольшим количеством C . Ядро система может быть расширена путем в плагин механизма. [4]
Название coq означает « петух » на французском языке и происходит от французской традиции называть инструменты разработки в честь животных. [5] Вплоть до 1991 года Coquand реализовывал язык под названием « Исчисление конструкций», а в то время он назывался просто CoC. В 1991 году была начата новая реализация, основанная на расширенном исчислении индуктивных построений, и название было изменено с CoC на Coq в косвенной ссылке на Coquand, который разработал Исчисление конструкций вместе с Жераром Хуэ и внес свой вклад в исчисление индуктивных построений. с Кристин Полин-Моринг. [6]
Coq предоставляет язык спецификаций под названием Gallina [7] (« курица » на латыни, испанском, итальянском и каталонском языках). Программы, написанные на Gallina, обладают слабым свойством нормализации , что означает, что они всегда завершаются. Это отличительное свойство языка, поскольку бесконечные циклы (программы без завершения) распространены в других языках программирования [8], и это один из способов избежать проблемы остановки .
Теорема о четырех цветах и расширение SSReflect
Жорж Гонтье из Microsoft Research в Кембридже , Англия, и Бенджамин Вернер из INRIA использовали Coq для создания доступного для обозрения доказательства теоремы о четырех цветах , которое было завершено в 2005 году. [9] Их работа привела к разработке SSReflect («Small Scale Reflection»). "), который был значительным расширением Coq. [10] Несмотря на название, большинство функций, добавленных в Coq с помощью SSReflect, являются функциями общего назначения и не ограничиваются вычислительным стилем доказательства. Эти функции включают:
- Дополнительное удобное для обозначения неопровержимого и опровержимого сопоставления с образцом , на индуктивных типах с одним или двумя конструкторами
- Неявные аргументы для функций, применяемых к нулевым аргументам, что полезно при программировании с функциями высшего порядка.
- Краткие анонимные аргументы
- Улучшенная
set
тактика с более мощным соответствием - Поддержка рефлексии
SSReflect 1.11 находится в свободном доступе, имеет двойную лицензию по лицензии CeCILL-B или CeCILL-2.0 с открытым исходным кодом и совместим с Coq 8.11. [11]
Приложения
- CompCert : оптимизирующий компилятор почти для всего языка программирования C, который в значительной степени запрограммирован и испытан на Coq.
- Структура данных с непересекающимся множеством : доказательство корректности в Coq было опубликовано в 2007 году [12].
- Теорема Фейта – Томпсона : формальное доказательство с использованием Coq было завершено в сентябре 2012 г. [13]
- Теорема о четырех цветах : формальное доказательство с использованием Coq было завершено в 2005 г. [9]
Смотрите также
- Нупрл
- Агда
- Идрис
- Расчет конструкций
- Переписка Карри – Ховарда
- Изабель (помощник по тестированию) - похожий / конкурирующий софт
- Интуиционистская теория типов
- HOL (помощник по проверке)
Рекомендации
- ^ "Coq 8.12.2 отсутствует" . 2020-12-11.
- ^ "Coq 8.13 + beta1 отсутствует" . 2020-12-07.
- ^ Краткое введение в Coq
- ^ Авигад, Джереми; Махбуби, Ассия (3 июля 2018 г.). Интерактивное доказательство теорем: 9-я международная конференция, ITP 2018, проходившая как ... ISBN 9783319948218. Проверено 21 октября 2018 года .
- ^ «Часто задаваемые вопросы» . Проверено 8 мая 2019 .
- ^ «Введение в исчисление индуктивных конструкций» . Проверено 21 мая 2019 .
- ^ Адам Хлипала. «Сертифицированное программирование с зависимыми типами»: «Библиотечные вселенные» .
- ^ Адам Хлипала. «Сертифицированное программирование с зависимыми типами»: «Библиотека GeneralRec» . «Библиотека InductiveTypes» .
- ^ а б Гонтье, Жорж (2008), «Формальное доказательство - теорема о четырех цветах» (PDF) , Уведомления Американского математического общества , 55 (11), стр. 1382–1393, MR 2463991
- ^ Жорж Гонтье, Ассия Махбуби. «Введение в мелкомасштабную рефлексию в Coq»: «Журнал формализованного мышления» .
- ^ «Библиотека математических компонентов 1.11.0» .
- ^ Кончон, Сильвен; Филлиатр, Жан-Кристоф (октябрь 2007 г.), «Постоянная структура данных поиска профсоюзов», Семинар ACM SIGPLAN по машинному обучению, Фрайбург, Германия
- ^ «Теорема Фейта-Томпсона полностью проверена в Coq» . Msr-inria.inria.fr. 2012-09-20. Архивировано из оригинала на 2016-11-19 . Проверено 25 сентября 2012 .
Внешние ссылки
- Помощник доказательства Coq - официальный английский сайт
- coq / coq - репозиторий исходного кода проекта на GitHub
- Интерактивная онлайн-система JsCoq - позволяет запускать Coq в веб-браузере без необходимости установки какого-либо программного обеспечения.
- Alectryon - библиотека для обработки фрагментов кода Coq, встроенных в документы, с отображением целей и сообщений для каждого предложения Coq.
- Coq Вики
- Библиотека математических компонентов - широко используемая библиотека математических структур, частью которой является язык доказательства SSReflect.
- Конструктивный репозиторий Coq в Неймегене
- Математические классы
- Coq в Open Hub
- Учебники
- The Coq'Art - книга Ива Берто и Пьера Кастерана о Coq
- Сертифицированное программирование с зависимыми типами - онлайн и печатный учебник Адама Члипала
- Основы программного обеспечения - онлайн-учебник Бенджамина К. Пирса и др.
- Введение в мелкомасштабное отражение в Coq - учебник по SSReflect от Жоржа Гонтье и Ассии Махбуби
- Учебники
- Введение в Coq Proof Assistant - видеолекция Эндрю Аппеля из Института перспективных исследований
- Видеоуроки для помощника по тестированию Coq от Андрея Бауэра.