Coq
Coq 是一個交互式的定理證明輔助工具。它允許用戶輸入包含數學斷言的表達式、機械化地對這些斷言執行檢查、幫助構造形式化的證明、並從其形式化描述的構造性證明中提取出可驗證的(certified)程序。Coq 的理論基礎是歸納構造演算(calculus of inductive constructions)、一種構造演算(calculus of constructions)的衍生理論。Coq 並非一個自動化定理機器證明語言;然而,它提供了自動化定理證明的策略(tactics)和不同的決策過程。
![]() | |
編程範型 | 函數式編程 |
---|---|
面市時間 | 1989年5月1日 | (版本4.10)
當前版本 |
|
型態系統 | 靜態類型,強類型 |
實作語言 | OCaml |
作業系統 | 跨平台 |
許可證 | LGPL 2.1 |
文件擴展名 | .v |
網站 | coq |
啟發語言 | |
ML(編程) LCF(證明方法) Automath(混合證明/編程) System F 和直覺類型論 | |
影響語言 | |
Agda,Idris, Matita, Albatross |
![](http://upload.wikimedia.org/wikipedia/commons/thumb/0/0d/CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png/300px-CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png)
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 語言本身並非圖靈完全。
應用
編輯引用
編輯- ^ Release Coq 8.19.2. 2024年6月10日 [2024年7月17日].
- ^ Coq 8.12.2 is out. 2020-12-11 [2021-08-29]. (原始內容存檔於2022-03-23).
- ^ Coq 8.13+beta1 is out. 2020-12-07 [2021-08-29]. (原始內容存檔於2022-04-07).
- ^ A short introduction to Coq (頁面存檔備份,存於網際網路檔案館).
- ^ PI.R2. [2014-01-23]. (原始內容存檔於2013-12-17).
- ^ Coq Version 8.0 for the Clueless (174 Hints) (頁面存檔備份,存於網際網路檔案館). Flint.cs.yale.edu. Retrieved on 2013-11-07.
- ^ Adam Chlipala. "Certified Programming with Dependent Types": "Library Universes" (頁面存檔備份,存於網際網路檔案館).
- ^ Adam Chlipala. "Certified Programming with Dependent Types": "Library GeneralRec" (頁面存檔備份,存於網際網路檔案館). "Library InductiveTypes" (頁面存檔備份,存於網際網路檔案館).
外部連結
編輯- http://coq.inria.fr/ (頁面存檔備份,存於網際網路檔案館) - the official Coq English website
- https://softwarefoundations.cis.upenn.edu (頁面存檔備份,存於網際網路檔案館) - Software Foundations