数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| 回数 | date | 内容(予定) | 資料 | 宿題 |
|---|
| 1 | 10/5 |
導入, Basics.v |
スライド0, スライド1 |
Coq 環境の構築，テキストのダウンロード
|
| 2 | 10/12 |
Basics.v, Induction.v |
スライド2 学生実験２のgitについての資料, GitHub での宿題提出
|
演習問題(締切 10/19 10:30: Basics.v の nandb, andb3, factorial, ltb, plus_id_exercise, zero_nbeq_plus_1)
(締切 10/26 10:30: Induction.v の basic_induction, double_plus, add_comm_informal, eqb_refl)
|
| 3 | 10/19 |
単純型付ラムダ計算 |
配布資料1 |
|
| 4 | 10/26 |
単純型付ラムダ計算(つづき) |
|
|
| 5 | 11/2 |
Lists.v |
スライド3 |
演習問題(締切 11/16 9:00:
Lists.v の snd_fst_is_swap, list_funs, list_exercises, eqblist, hd_error)
|
| 6 | 11/9 |
Poly.v |
スライド4
|
演習問題(締切 11/23 9:00:
Poly.v の poly_exercises, split, flat_map, currying)
|
| 7 | 11/16 |
多相ラムダ計算 System F |
配布資料2
問題集
|
随意課題(締切 11/30 9:00: 問題集1〜3節の問題を解いて，解答を書いた pdf を PandA でアップロードする．)
|
| 8 | 11/30 |
ハイブリッド演習 |
|
| 9 | 12/7 |
Tactics.v |
スライド5
|
演習問題(締切 12/21 9:00:
Tactics.v の apply_exercises1, injection_ex3, discriminate_ex3, eqb_true, destruct_eqn_practice)
|
| 10 | 12/14 |
Logic.v |
スライド6
|
演習問題(締切 1/11 9:00:
Logic.v の and_assoc, contrapositive, not_both_true_and_false,
or_distributes_over_and, dist_exists_or, In_app_iff,
logical_connectives)
|
| 11 | 12/21 |
自然演繹と Coq |
配布資料3
|
随意課題(締切 1/18 9:00: 問題集4〜6節の問題を解いて，解答を書いた pdf を PandA でアップロードする．)
|
| 12 | 12/28 (は？) |
IndProp.v |
スライド7 |
演習問題(締切 1/18 9:00:
IndProp.v の ev_double, inversion_practice, ev_sum, le_exercises の一部
(le_trans と O_le_n と le_plus_l)
|
| 13 | 1/11 |
カリーハワード同型対応，ProofObjects.v |
配布資料４, スライド8 |
|
|
| 14 | 1/18 |
ハイブリッド演習 |
|
| 期末試験 | ? |
|
|
|