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 のダウンロード
  • Windows
  • MacOS / Arm
  • MacOS / Intel
• CoqIDEが文字化けをしたらVSCodeを使いましょう
  • WindowsのVScodeでCoqを使う（初心者向け）
• 何もインストールせずに 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チュートリアル（日本語）