Интернет магазин китайских планшетных компьютеров

Компьютеры - Coq - Инструменты

• Язык реализации — OCaml и Си
• Лицензия — GNU Lesser General Public Licence Version 2.1
• Среды разработки:
  • Компилятор coqc и инструменты для работы с проектами, состоящими из множества файлов
  • coqtop — консольная интерактивная среда
  • Среды разработки с графическим интерфейсом пользователя:
    • CoqIDE
    • Eclipse Proof General
    • Режим для Emacs
• coqdoc — генератор документации к библиотекам, выход в LaTeX и HTML
• Экспорт доказательств в XML для проектов HELM1 и MoWGLI
• Конструктивная математика известна тем, что из доказательства существования величины можно экстрагировать алгоритм получения этой величины. Coq может экспортировать алгоритмы в языки ML и Haskell. Значения, имеющие тип, принадлежащий сорту Prop, не экстрагируются; обычно эти значения есть доказательства.
• Coq можно расширять, не ухудшая надёжности. Корректность проверки доказательств зависит от proof-checker, который есть небольшая часть от всего проекта. Он проверяет доказательства, сгенерированные тактиками, поэтому некорректная тактика не приводит к принятию доказательства с ошибкой. Таким образом, Coq следует принципу де Брюина.