Coq

Coq (программное обеспечение)

Разработчики)	Команда разработчиков Coq
Начальная версия	1 мая 1989 г . ; 32 года назад (версия 4.10) ( 1989-05-01 )

Стабильный выпуск	8.13.1 ^[1] / 22 февраля 2021 г . ; 9 месяцев назад ( 2021-02-22 )
Предварительный выпуск	8.13 + beta1 ^[2] / 7 декабря 2020 г . ; 12 месяцев назад ( 07.12.2020 )

Репозиторий	github .com / coq / coq
Написано в	OCaml
Операционная система	Кроссплатформенность
Доступно в	английский
Тип	Помощник доказательства
Лицензия	LGPLv2.1
Веб-сайт	coq .inria .fr

Интерактивный сеанс доказательства в CoqIDE, показывающий сценарий доказательства слева и состояние доказательства справа.

Coq - это интерактивное средство доказательства теорем, впервые выпущенное в 1989 году. Оно позволяет выражать математические утверждения, механически проверяет доказательства этих утверждений, помогает находить формальные доказательства и извлекает сертифицированную программу из конструктивного доказательства ее формальной спецификации . Coq работает в рамках теории исчисления индуктивных построений , производной от исчисления построений . Coq не является автоматическим средством доказательства теорем, но включает в себя тактику ( процедуры ) автоматического доказательства теорем и различные процедуры принятия решений .

Ассоциация вычислительной техники награждена Тьерри Кокана , Gérard HUET , Кристин Паулина-Möhring , Бруно Баррас, Жан-Кристоф Filliâtre Уго Herbelin, Четан Мурти, Ив Берто, и Пьер Castéran с 2013 годом премией ACM Software System для Coq.

Coq - это игра слов от имени Тьерри Коквана, Calculus of Constructions или «CoC», которая следует французской традиции называть инструменты в честь животных ( coq по-французски означает петух). ^[3]

Обзор

Если рассматривать как язык программирования, Coq реализует функциональный язык программирования с зависимой типизацией ; ^[4], если рассматривать ее как логическую систему, она реализует теорию типов более высокого порядка . Разработка Coq с 1984 года поддерживается INRIA , теперь в сотрудничестве с École Polytechnique , Университетом Париж-Юг , Парижским университетом Дидро и CNRS . В 1990-х годах ENS Lyon также был частью проекта. Разработка Coq была инициирована Жераром Юэ и Тьерри Коканом, и с момента ее создания более 40 человек, в основном исследователи, внесли свой вклад в основную систему. Группу внедрения последовательно координировали Жерар Юэ, Кристин Полен-Моринг, Уго Эрбелен и Матье Созо. Coq в основном реализуется в OCaml с небольшим количеством C . Ядро система может быть расширена путем в плагин механизма. ^[5]

Название coq по- французски означает « петух » и происходит от французской традиции называть инструменты разработки в честь животных. ^[6] Вплоть до 1991 года Кокванд реализовывал язык под названием « Исчисление конструкций», а в то время он назывался просто CoC. В 1991 году была начата новая реализация, основанная на расширенном исчислении индуктивных построений, и название было изменено с CoC на Coq в косвенной ссылке на Кокванда, который разработал Исчисление конструкций вместе с Жераром Хуэ и внес свой вклад в Исчисление индуктивных построений. с Кристин Полин-Моринг. ^[7]

Coq предоставляет язык спецификаций под названием Gallina ^[8] (« курица » на латыни, испанском, итальянском и каталонском языках). Программы, написанные на Gallina, обладают слабым свойством нормализации , что означает, что они всегда завершаются. Это отличительное свойство языка, поскольку бесконечные циклы (программы без завершения) распространены в других языках программирования ^[9], и это один из способов избежать проблемы остановки .

Доказательство коммутативности сложения натуральных чисел в Coq.
plus_comm = fun n m : nat => nat_ind ( fun n0 : nat => n0 + m = m + n0 ) ( plus_n_0 m ) ( fun ( y : nat ) ( H : y + m = m + y ) => eq_ind ( S ( m + y )) ( забава n0 : nat => S ( y + m ) = n0 ) ( f_equal S H ) ( m + S y ) ( plus_n_Sm m y )) n : для всех n m : nat , n + m = m + n
`nat_ind`означает математическую индукцию , `eq_ind`замену равных и `f_equal`взятие одной и той же функции по обе стороны от равенства. Ссылки на более ранние теоремы показывают и . ${\ displaystyle m = m + 0}$ ${\ Displaystyle S (m + y) = m + Sy}$

Теорема четырех цветов и расширение SSReflect

Джорджес Гонтье из Microsoft Research в Кембридже , Англия, и Бенджамин Вернер из INRIA использовали Coq для создания проверяемого доказательства теоремы о четырех цветах , которое было завершено в 2002 году. ^[10] Их работа привела к разработке SSReflect («Small Scale Reflection»). "), который был значительным расширением Coq. ^[11] Несмотря на название, большинство функций, добавленных в Coq с помощью SSReflect, являются функциями общего назначения и не ограничиваются вычислительным стилем доказательства. Эти функции включают:

Дополнительное удобное для обозначения неопровержимого и опровержимого сопоставления с образцом , на индуктивных типах с одним или двумя конструкторами
Неявные аргументы для функций, применяемых к нулевым аргументам, что полезно при программировании с функциями высшего порядка.
Краткие анонимные аргументы
Улучшенная setтактика с более мощным соответствием
Поддержка рефлексии

SSReflect 1.11 находится в свободном доступе, имеет двойную лицензию по лицензии CeCILL-B или CeCILL-2.0 с открытым исходным кодом и совместим с Coq 8.11. ^[12]

Приложения

CompCert : оптимизирующий компилятор почти для всего языка программирования C, который в значительной степени запрограммирован и испытан на Coq.
Структура данных с непересекающимся множеством : доказательство корректности в Coq было опубликовано в 2007 году ^[13].
Теорема Фейта – Томпсона : формальное доказательство с использованием Coq было завершено в сентябре 2012 г. ^[14]
Теорема о четырех цветах : формальное доказательство с использованием Coq было завершено в 2005 г. ^[10]

Смотрите также

Нупрл
Агда
Идрис
Расчет конструкций
Переписка Карри – Ховарда
Изабель (помощник по пруфу) - похожее / конкурирующее программное обеспечение
Интуиционистская теория типов
HOL (помощник проверки)

использованная литература

^ "Coq 8.13.1 отсутствует" . 2021-02-22.
^ "Coq 8.13 + beta1 отсутствует" . 2020-12-07.
^ "Альтернативные имена · coq / coq Wiki" . GitHub . Проверено 11 ноября 2021 .
^ Краткое введение в Coq
↑ Авигад, Джереми; Махбуби, Ассия (3 июля 2018 г.). Интерактивное доказательство теорем: 9-я международная конференция, ITP 2018, проходившая как ... ISBN 9783319948218. Проверено 21 октября 2018 года .
^ «Часто задаваемые вопросы» . Проверено 8 мая 2019 .
^ «Введение в исчисление индуктивных конструкций» . Проверено 21 мая 2019 .
^ Адам Хлипала. «Сертифицированное программирование с зависимыми типами»: «Библиотечные вселенные» .
^ Адам Хлипала. «Сертифицированное программирование с зависимыми типами»: «Библиотека GeneralRec» . «Библиотека InductiveTypes» .
^ a b Gonthier, Georges (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 / coq - репозиторий исходного кода проекта на GitHub
Интерактивная онлайн-система JsCoq - позволяет запускать Coq в веб-браузере без необходимости установки какого-либо программного обеспечения.
Alectryon - библиотека для обработки фрагментов кода Coq, встроенных в документы, с отображением целей и сообщений для каждого предложения Coq.
Coq Вики
Библиотека математических компонентов - широко используемая библиотека математических структур, частью которой является язык доказательства SSReflect.
Конструктивный репозиторий Coq в Неймегене
Математические классы
Coq в Open Hub

Учебники

The Coq'Art - книга Ива Берто и Пьера Кастерана о Coq
Сертифицированное программирование с зависимыми типами - онлайн и печатный учебник Адама Члипала
Основы программного обеспечения - онлайн-учебник Бенджамина К. Пирса и др.
Введение в мелкомасштабное отражение в Coq - учебник по SSReflect от Жоржа Гонтье и Ассии Махбуби

Учебники

Введение в Coq Proof Assistant - видеолекция Эндрю Аппеля из Института перспективных исследований
Видеоуроки для помощника по тестированию Coq от Андрея Бауэра.

[1] "Coq 8.13.1 отсутствует" . 2021-02-22.

[2] "Coq 8.13 + beta1 отсутствует" . 2020-12-07.

[3] "Альтернативные имена · coq / coq Wiki" . GitHub . Проверено 11 ноября 2021 .

[4] Краткое введение в Coq

[5] Авигад, Джереми; Махбуби, Ассия (3 июля 2018 г.). Интерактивное доказательство теорем: 9-я международная конференция, ITP 2018, проходившая как ... ISBN 9783319948218. Проверено 21 октября 2018 года .

[6] «Часто задаваемые вопросы» . Проверено 8 мая 2019 .

[7] «Введение в исчисление индуктивных конструкций» . Проверено 21 мая 2019 .

[8] Адам Хлипала. «Сертифицированное программирование с зависимыми типами»: «Библиотечные вселенные» .

[9] Адам Хлипала. «Сертифицированное программирование с зависимыми типами»: «Библиотека GeneralRec» . «Библиотека InductiveTypes» .

[:0-10] Gonthier, Georges (2008), «Формальное доказательство - теорема о четырех цветах» (PDF) , Уведомления Американского математического общества , 55 (11), стр. 1382–1393, MR 2463991

[11] Жорж Гонтье, Ассия Махбуби. «Введение в мелкомасштабную рефлексию в Coq»: «Журнал формализованного мышления» .

[12] "Библиотека математических компонентов 1.11.0" .

[13] Кончон, Сильвен; Филлиатр, Жан-Кристоф (октябрь 2007 г.), «Постоянная структура данных поиска профсоюзов», Семинар ACM SIGPLAN по машинному обучению, Фрайбург, Германия

[14] "Теорема Фейта-Томпсона была полностью проверена в Coq" . Msr-inria.inria.fr. 2012-09-20. Архивировано из оригинала на 2016-11-19 . Проверено 25 сентября 2012 .

[1]