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

レポート課題

• レポート課題 提出期限 2019年1月28日(月)

講義予定

第1回 10月3日

Coq で関数型プログラミング

• 講義メモ
• 資料 EmacsでCoqを使う
• 設定ファイル coq.emacs (.emacs にコピーす る)
• ProofGeneral PG-master.zip (Safariでダウンロードする)

第2回 10月10日

Coqの論理

• 講義メモ

第3回 10月17日

述語論理と帰納法

• 講義メモ

第4回 11月7日

帰納的な定義と多相性

• 講義メモ

第5回 11月14日

多相性と単一化

• 講義メモ

第6回 11月21日

プログラムの証明1

• 講義メモ

第7回11月28日

プログラムの証明2

• 講義メモ

第8回12月5日

数学的な証明

• 講義メモ

第9回12月12日

MathComp/SSReflect

• 講義メモ
• ssrbool_doc.pdf, ssrnat_doc.pdf (R. Affeldt の SSReflect Tutorial より)

第10回 12月19日

MathComp/SSReflect 2

• 講義メモ
• coq10.v
• bigo_doc.pdf

第11回 1月9日

コンパイラ

• 講義メモ
• coq10a.v
• coq11.v

第12回 1月16日

ラムダ計算

• 講義メモ
• λ計算について
• coq11a.v
• coq12.v

最終回 1月23日

線形代数

• 講義メモ
• coq12a.v (前回の解)
• coq13.v
• coq13a.v (今回の解)

MathComp/SSReflect

• Download mathcomp-1.7.0-media.tgz

• % cd ~
  % tar zxvf Desktop/mathcomp-1.7.0-media.tgz      #Firefoxの場合
  % tar zxvf Downloads/mathcomp-1.7.0-media.tgz    #Safariの場合
  

• ソースは mathcomp-1.7.0.tar.gz
• 構文のマニュアルは ここ
• ドキュメントは ここ

Coq に関する情報源

Coq@INRIA

開発元 (英語)

Proof Café

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

プログラミングCoq

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

MathComp@Github

MathCompの開発元 (英語)

SSReflect チュートリアル

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