2014年度前期・数理解析・計算機数学 II (同 概論II)

レポート課題

• レポート課題 提出期限 2014年7月31日(木)

講義予定

第1回 4月14日

Coq で関数型プログラミング

• 講義メモ
• 資料 EmacsでCoqを使う
• 設定ファイル coq.emacs (.emacs にコピーす る)

第2回 4月21日

Coqの論理

• 講義メモ

第3回 4月28日

述語論理と帰納法

• 講義メモ

第4回 5月12日

帰納的な定義と多相性

• 講義メモ

第5回 5月19日

プログラムの証明1

• 講義メモ

5月25日 13時半〜17時半 A館207号室 (ご興味の方)

Proof Cafe: 先輩達によるCoqの勉強会

第6回 5月26日

プログラムの証明1

第7回 6月2日

プログラムの証明2

• 講義メモ

第8回 6月9日

数学的な証明

• 講義メモ

第9回 6月16日

命題論理の意味論

• 講義メモ

第10回 6月23日

命題論理の証明論

• 講義メモ
• coq10.v

第11回 6月30日

証明論の完全性

• 講義メモ
• coq11.v

第12回 7月7日

証明論の完全性(2)

• coq11b.v 前回のprovable_nnfまで

第13回 7月14日

単一化と応用

• 講義メモ
• coq12.v
• coq11b.v 前回の解答

第13回 7月28日

単一化の完全性

• 講義メモ
• coq13.v

Coq に関する情報源

Coq@INRIA

開発元 (英語)

Proof Café

名古屋におけるCoqや関数型言語の情報

プログラミングCoq

IIJのCoqチュートリアル（日本語）