[ ホーム
| 講義 ]
2024年度春・数理解析・計算機数学 IV (同 概論IV)
- 時間
- 水曜日 1・2限
- 教室
- 多元 409
講義予定
- シラバス (4月22日更新)
- 注意:毎回の課題の提出はTACTのメッセージで行って下さい
- 第1回 4月10日
- Coq/SSReflectの論理
- 第2回 4月17日
- 述語論理とSSReflectのタクティック
- 第3回 4月24日
- 再帰的な定義と帰納法
--
- 第4回 5月1日
- 帰納的な定義と型付け
- 第5回 5月8日
- Mathcomp, 自己反映と数論の証明
- 5月15日 休講
Coq/MathComp/SSReflect
- Coq platform 2023.11.0 / MathComp 1.18
または 2023.03.0 / Coq 8.17.1 のダウンロード
- CoqIDEが文字化けをしたらVSCodeを使いましょう
- 何もインストールせずに Chrome の中
で jsCoq を実行することもできる
Coq に関する情報源
- Coq@INRIA
- 開発元 (英語)
- Coq
Platform
- 最新版のダウンロード
- Programs and Proofs
- Ilya Sergey の講義ノート (英語)
- MathComp@Github
- MathCompの開発元 (英語)
- SSReflect
チュートリアル
- Reynald AffeldtによるCoqのチュートリアル (日本語あり)
- Proof Café
- 名古屋におけるCoqや関数型言語の情報
- プログラミングCoq
- IIJのCoqチュートリアル(日本語)
最終更新2024.5.1