Coq
Coq(コック)
定理証明支援系
のシステムの一つ
Coq自体がどんな理論に乗っかって作られているかは主に以下
依存型理論
Calculus of Inductive Constructions(CIC)
Gallina
Vernacular
インストール
Coq インストール
公式:
Welcome! | The Coq Proof Assistant
入門系？
『プログラミング Coq』池渕未来
ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation
ドキュメント
The Coq library — Coq 8.17.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』
#形式手法