[ ホーム | 講義 ]

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

レポート課題

講義予定

シラバス

第1回 10月7日
Coq で関数型プログラミング

第2回 10月14日
Coqの論理

第3回 10月21日
述語論理と帰納法

第4回 10月28日
帰納的な定義と多相性

第5回 11月4日
多相性と単一化

第6回 11月11日
プログラムの証明1

第7回11月18日
プログラムの証明2

第8回11月25日
数学的な証明

第9回12月2日
SSReflect

第10回 12月 9日
SSReflect 2

第11回 12月16日
SSReflect 3

第12回 1月13日
コンパイラ

第13回 1月20日
ラムダ計算

第14回 1月27日
λ計算

SSReflect

Coq に関する情報源

Coq@INRIA
開発元 (英語)
Proof Café
名古屋におけるCoqや関数型言語の情報
プログラミングCoq
IIJのCoqチュートリアル(日本語)
SSReflect@MSR
SSReflectの開発元 (英語)
SSReflect チュートリアル
Reynald AffeldtによるCoqのチュートリアル (日本語あり)

最終更新2016.1.27