Coq - PukiWikiCoq † http://coq.inria.fr/ Coq は、INRIA にて開発されている対話的定理証明支援系です。 Calculus of Inductive Construction (CIC) を基礎とし、Tactics と呼ばれるコマンドを駆使することにより証明を行います。 ↑ メモ † インストールする Coq 本体 Proofgeneral 証明をやってみる 簡単なものから Tactics リスト 証明の裏で何が起こっているのか 証明の実例 理論的 background Dependently Typed Lambda Calculus Curry-Howard Isomorphism ぼちぼち書いていきます。 ↑
