[ ホーム | 講義 ]

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

レポート課題

講義予定

シラバス

第1回 4月16日
Coq/SSReflectの論理

第2回 4月23日
述語論理とSSReflectのタクティク

第3回 5月8日
再帰的な定義と帰納法

第4回 5月15日
帰納的な定義と自己反映

第5回 5月22日
単一化と数論

第6回 5月29日
プログラムの証明

第7回 6月5日
Curry-Howard対応

第8回 6月12日
命題論理の意味論

第9回 6月19日
命題論理の証明論

第10回 6月26日
命題論理の証明論

第11回 7月 3日
数学:自然数・実数・総和

第12回 7月 10日
続 総和

7月 10日 (休講)

第13回 7月 24日
線形代数

MathComp/SSReflect

Coq に関する情報源

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

最終更新2019.7.23