[
ホーム
|
講義
]
2015年度後期・数理解析・計算機数学 II (同 概論II)
レポート課題
レポート課題
提出期限 2016年2月3日(水)
講義予定
シラバス
第1回 10月7日
Coq で関数型プログラミング
講義メモ
資料
EmacsでCoqを使う
設定ファイル
coq.emacs
(.emacs にコピーす る)
第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
講義メモ
coq10.v
第11回 12月16日
SSReflect 3
講義メモ
coq11.v
第12回 1月13日
コンパイラ
講義メモ
coq11.v
coq12.v
第13回 1月20日
ラムダ計算
講義メモ
λ計算について
第14回 1月27日
λ計算
講義メモ
(前回の訂正と追加)
coq13.v
(講義後更新)
SSReflect
Dowload
ssreflect-1.5-media.tgz
% cd ~ % tar zxvf Desktop/ssreflect-1.5-media.tgz
Coq に関する情報源
Coq@INRIA
開発元 (英語)
Proof Café
名古屋におけるCoqや関数型言語の情報
プログラミングCoq
IIJのCoqチュートリアル(日本語)
SSReflect@MSR
SSReflectの開発元 (英語)
SSReflect チュートリアル
Reynald AffeldtによるCoqのチュートリアル (日本語あり)
最終更新2016.1.27