Coqで学ぶ定理証明入門メモ

2300 ワード
Coq Coq テキストリンク

edubase Streamで配信していた、『Coqで学ぶ定理証明入門』を見てみたのでそのメモ。

概要

講師がCoqを使って簡単な例題を解きながら操作を説明し、
それにあわせて実際に手を動かしながら操作を体験することでCoqの使い方を学べる。
演習もあるので、説明を受けた操作をどう組み合わせるかなーといったことを考えながら試行錯誤できる。

定理証明を進めるためのツールとしてCoqの使い方に慣れましょう、という内容なので、
定理証明を学習するという目的には適していないと思う。

また、最後にオンラインドキュメントや書籍、勉強会などの参考情報があるので、
この講義を受けた後のアクションプランも分かりやすいかなと思う。

ただし、2011年の集中講義の内容らしいので、色々古い情報もある。
（特に勉強会とか）

時間

4.5時間程度。

  • 動画は3分割されていて、1.5時間、1.5時間、1時間くらい。
  • 上記に加えて、演習に0.5時間くらいかけた。

内容

略。時間があったら追記する。

TODO

最後の演習が残なのでやる。

参考情報（と紹介されているもの）

Coq本家のリファレンス

  • 本家は王道

Jacques Garrigue先生の講義資料

  • 数理解析・計算機数学がCoqの使い方っぽい

CPDT

  • Coqのすごい人の講義資料

Coqt

  • IIJのアルバイトの方が書いたCoqの入門記事

Coq'Art

  • Coqの中身についてもがっつり書いている

fm-forum

  • 形式手法についての勉強会

ProofCafe

Proof Summit

函数プログラムの集い