Coq 是一個交互式的定理證明輔助工具。它允許用戶輸入包含數學斷言的表達式、機械化地對這些斷言執行檢查、幫助構造形式化的證明、並從其形式化描述的構造性證明中提取出可驗證的（certified）程序。Coq 的理論基礎是歸納構造演算（calculus of inductive constructions）、一種構造演算（calculus of constructions）的衍生理論。Coq 並非一個自動化定理機器證明語言；然而，它提供了自動化定理證明的策略（tactics）和不同的決策過程。
Coq 同時還是一個依賴類型的函數式程式語言[4]。它由法國PPS實驗室的PI.R2團隊研究開發[5]，該團隊由INRIA、巴黎綜合理工學院、巴黎第十一大學、巴黎第七大學和法國國家科學研究中心組成。此前里昂高等師範學校亦曾參與開發。Coq 項目當前由 Gérard Huet、Christine Paulin-Mohring 和 Hugo Herbelin領導。Coq 使用 OCaml 以及少部分 C 實現。
單詞 coq 在法語中意為「公雞」，此命名體現了法國在研究活動中使用動物名稱命名工具的傳統。[6] 最初，它被簡單地稱作 Coc，意即構造演算（calculus of constructions）的縮寫，同時也暗含了 Thierry Coquand（與 Gérard Huet 共同提出了前述的構造演算）的姓氏。
Coq 自身提供了一套規範語言 Gallina[7] （gallina 在西班牙語中意為「母雞」）。使用 Gallina 書寫的程序具有規範化性質——它們總是會終止。此性質使之避開了停機問題 [8]。同時，這也使得 Coq 語言本身並非圖靈完全。
應用
引用
外部連結
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
