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

レポート課題

• レポート課題 提出期限 2013年8月2日(金)

講義予定

第1回 4月12日

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

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

第2回 4月19日

Coqの論理

• 講義メモ

第3回 4月26日

述語論理と帰納法

• 講義メモ

第4回 5月10日

帰納的な定義と多相性

• 講義メモ

第5回 5月17日

プログラムの証明1

• 講義メモ

第6回 5月24日

プログラムの証明1

5月25日 14時半〜17時半 多元307号室 (ご興味の方)

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

第7回 5月31日

プログラムの証明2

• 講義メモ

6月7日　名大際のため休講

第8回 6月14日

数学的な証明

• 講義メモ

第9回 6月21日

命題論理の意味論

• 講義メモ

第10回 6月28日

命題論理の証明論

• 講義メモ

第11回 7月5日

命題論理の完全性

第12回 7月12日

単一化と応用

• 講義メモ

第13回 7月19日

単一化の完全性

• 講義メモ

第14回 7月26日

導出原理

• 講義メモ

Coq に関する情報源

Coq@INRIA

開発元 (英語)

Proof Café

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

プログラミングCoq

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