Математика - Coq

Coq - это вспомогательный инструмент для доказательств в высокоуровневой логике, который делает разработку компьютерных программ совметимой с их формальным описанием. Он разработан с использованием Objective Caml и Camlp5.

Система Coq предоставляет язык Gallina (Курица) — функциональный язык с зависимыми типами, основанный на исчислении индуктивных конструкций. Особенностью данной системы является наличие особого подъязыка тактик доказательства (в отличии от, например, Агды, в которой пользователь конструирует элемент типа, являющийся доказательством, в явном виде с использованием интерактивного интерфейса, основанного на Emacs).

Coq используется как собственно в математике, так и для так называемого сертифицированного программирования — написания программ вместе с доказательством их корректности.

В состав пакета входит coqtop - интерфейс командной строки для Coq.

Графический интерфейс пользователя для Coq предоставлен пакетом coqide. Coq может быть также использован с ProofGeneral, который позволяет редактировать доказательства, используя emacs и xemacs. Для этого потребуется установить пакет proofgeneral-coq.

Сайт разработчика: http://coq.inria.fr/
Что почитать?

• Coq. Материал из Википедии