2021年前期・数理科学特論8

レポート課題

• レポート課題 提出期限 2021年7月16日(金)

第1回6月28日

Coq/SSReflectの論理

• 講義メモ
• 資料 EmacsでCoqを使う
• 設定ファイル coq.emacs

第2回6月29日

述語論理とSSReflectのタクティック

• 課題の答え

第3回6月30日

再帰的な定義と帰納法

• 課題の答え

第4回7月1日

Mathcompと自己反映・数の証明

• ssrbool_doc.pdf, ssrnat_doc.pdf (R. Affeldt の SSReflect Tutorial より)
• 課題の答え

第5回7月2日

プログラムの証明

Coq に関する情報源

Coq@INRIA

開発元 (英語)

Coq atform

最新版のダウンロード

Programs and Proofs

Ilya Sergey の講義ノート (英語)

MathComp@Github

MathCompの開発元 (英語)

SSReflect チュートリアル

Reynald AffeldtによるCoqのチュートリアル (日本語あり)

Proof Café

名古屋におけるCoqや関数型言語の情報

プログラミングCoq

IIJのCoqチュートリアル（日本語）