2021年度秋・数理解析・計算機数学 IV (同 概論IV)

レポート課題

• レポート課題 提出期限 2022年2月2日(水)

時間

水曜日 1・2限

教室

理学部 B-114

講義予定

• シラバス

第1回10月 6日

Coq/SSReflectの論理

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

第2回10月13日

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

• 講義メモ

第3回10月20日

再帰的な定義と帰納法

• 講義メモ

第4回10月27日

帰納的な定義と多相性

• 講義メモ

第5回11月10日

Mathcomp, 自己反映と数論の証明

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

第6回 11月17日

単一化と自動化

• 講義メモ

第7回 11月24日

プログラムの証明

• 講義メモ

第8回 12月1日

Mathcompでのプログラム証明

• 講義メモ

第9回 12月 8日

数学:自然数・実数・総和

• 講義メモ
• コード: ssrcoq9.v
• bigop_doc.pdf (R. Affeldt の SSReflect Tutorial より)

第10回 12月 9日

線形代数

• 講義メモ
• コード: ssrcoq10.v

第11回 12月22日

量子計算

• 講義メモ
• コード: ssrcoq11.v qecc library

第12回 1月12日

コンパイラ

• 講義メモ
• コード: ssrcoq11a.v ssrcoq12.v

第13回 1月19日

λ計算の簡約器

• 講義メモ
• コード: ssrcoq13.v

第14回 1月26日

代数的拡張

• 講義メモ
• コード: ssrcoq14.v

MathComp/SSReflect

• Download coq-8.9-mathcomp-1.11.0.tgz

• % cd ~
  % tar zxvf Desktop/coq-8.9-mathcomp-1.11.0.tgz      #Firefoxの場合
  % tar zxvf Downloads/coq-8.9-mathcomp-1.11.0.tgz    #Safariの場合
  

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

Coq に関する情報源

Coq@INRIA

開発元 (英語)

Coq Platform

最新版のダウンロード

Programs and Proofs

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

MathComp@Github

MathCompの開発元 (英語)

SSReflect チュートリアル

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

Proof Café

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

プログラミングCoq

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