[
ホーム
|
講義
]
2017年度後期・数理解析・計算機数学 II (同 概論II)
レポート課題
レポート課題
提出期限 2018年1月24日(水)
講義予定
シラバス
第1回 10月4日
Coq で関数型プログラミング
講義メモ
資料
EmacsでCoqを使う
設定ファイル
coq.emacs
(.emacs にコピーす る)
第2回 10月11日
Coqの論理
講義メモ
第3回 10月28日
述語論理と帰納法
講義メモ
第4回 10月25日
帰納的な定義と多相性
講義メモ
第5回 11月1日
多相性と単一化
講義メモ
第6回 11月8日
プログラムの証明1
講義メモ
11月15日
休講
第7回11月22日
プログラムの証明2
講義メモ
第8回11月29日
数学的な証明
講義メモ
12月6日
TPP参加のため休講
TPPmark 2017
第9回12月13日
MathComp/SSReflect
講義メモ
第10回 12月 9日
MathComp/SSReflect 2
講義メモ
coq10.v
ssrbool_doc.pdf
,
ssrnat_doc.pdf
(R. Affeldt の
SSReflect Tutorial
より)
第11回 12月20日
MathComp/SSReflect 3
講義メモ
coq11.v
第12回 1月10日
コンパイラ
講義メモ
coq11a.v
coq12.v
第13回 1月20日
ラムダ計算
講義メモ
λ計算について
coq12a.v
coq13.v
MathComp/SSReflect
Download
mathcomp-1.6-media.tgz
% cd ~ % tar zxvf Desktop/mathcomp-1.6-media.tgz
ソースは
mathcomp-1.6.tar.gz
ドキュメントは
ここ
Coq に関する情報源
Coq@INRIA
開発元 (英語)
Proof Café
名古屋におけるCoqや関数型言語の情報
プログラミングCoq
IIJのCoqチュートリアル(日本語)
SSReflect@MSR
SSReflectの開発元 (英語)
SSReflect チュートリアル
Reynald AffeldtによるCoqのチュートリアル (日本語あり)
最終更新2018.1.17