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

レポート課題

• レポート課題 提出期限 2018年1月24日(水)

講義予定

第1回 10月4日

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

• 講義メモ
• 資料 EmacsでCoqを使う
• 設定ファイル coq.emacs (.emacs にコピーす る)

第2回 10月11日

Coqの論理

• 講義メモ

第3回 10月28日

述語論理と帰納法

• 講義メモ

第4回 10月25日

帰納的な定義と多相性

• 講義メモ

第5回 11月1日

多相性と単一化

• 講義メモ

第6回 11月8日

プログラムの証明1

• 講義メモ

11月15日

休講

第7回11月22日

プログラムの証明2

• 講義メモ

第8回11月29日

数学的な証明

• 講義メモ

12月6日

TPP参加のため休講

TPPmark 2017

第9回12月13日

MathComp/SSReflect

• 講義メモ

第10回 12月 9日

MathComp/SSReflect 2

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

第11回 12月20日

MathComp/SSReflect 3

• 講義メモ
• coq11.v

第12回 1月10日

コンパイラ

• 講義メモ
• coq11a.v
• coq12.v

第13回 1月20日

ラムダ計算

• 講義メモ
• λ計算について
• coq12a.v
• coq13.v

MathComp/SSReflect

• Download mathcomp-1.6-media.tgz

• % cd ~
  % tar zxvf Desktop/mathcomp-1.6-media.tgz
  

• ソースは mathcomp-1.6.tar.gz
• ドキュメントは ここ

Coq に関する情報源

Coq@INRIA

開発元 (英語)

Proof Café

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

プログラミングCoq

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

SSReflect@MSR

SSReflectの開発元 (英語)

SSReflect チュートリアル

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