[ ホーム | 講義 ]

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

レポート課題

講義予定

第1回10月 7日
Coq/SSReflectの論理

第2回10月14日
述語論理とSSReflectのタクティック

第3回10月21日
再帰的な定義と帰納法

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

第5回11月4日
Mathcomp, 自己反映と単一化

第6回 11月11日
数の証明

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

第8回 11月25日
Mathcompでのプログラム証明

第9回 12月 2日
数学:自然数・実数・総和

第10回 12月 9日
線形代数

第11回 12月16日
コンパイラ

第12回 12月23日
λ計算の簡約器

第13回 1月13日
単一化の証明

第14回 1月20日
単一化の証明 (完全性)

MathComp/SSReflect

Coq に関する情報源

Coq@INRIA
開発元 (英語)
Coq 8.12.0
最新版のダウンロード
Programs and Proofs
Ilya Sergey の講義ノート (英語)
MathComp@Github
MathCompの開発元 (英語)
SSReflect チュートリアル
Reynald AffeldtによるCoqのチュートリアル (日本語あり)
Proof Café
名古屋におけるCoqや関数型言語の情報
プログラミングCoq
IIJのCoqチュートリアル(日本語)

最終更新2021.1.19