Coq
Coq(コック)
定理証明支援系
のシステムの一つ
Coq自体がどんな理論に乗っかって作られているかは主に以下
pCIC(predicative Calculus of Inductive Construcions)
型が
可述的
(階層的)であることを強調した
Calculus of Inductive Constructions(CIC)
に見える
依存型理論
Gallina
Vernacular
コマンド言語
インストール
Coq インストール
公式:
Welcome! | The Coq Proof Assistant
入門系？
『プログラミング Coq』池渕未来
ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation
ドキュメント
Introduction and Contents — Coq 8.20.0 documentation
ライブラリ
SSReflect
Coq-HoTT:
HoTT/Coq-HoTT: A Coq library for Homotopy Type Theory
UniMath
CompCert
というものがある
これは
DeepSpec
という団体？で作られたものとのこと
参考
『プログラミング Coq』池渕未来
HoTT/Coq 覚書
『History of Interactive Theorem Proving』
メモ
pCICについて - Sis puella magica!
誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記 (はてなBlog)
業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2） - 檜山正幸のキマイラ飼育記 (はてなBlog)
#形式手法