数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| 回数 | date | 内容(予定) | 資料 | 宿題 |
|---|
| 1 | 10/1 | 導入・オンライン教科書のインストール | スライド | Basics.v の予習 |
| 2 | 10/8 | Basics.v (Coq による関数型プログラミング) | スライド | 演習問題(締切 10/22 10:30: nandb, andb3, factorial, blt_nat)，Induction.v の予習 |
| 3 | 10/22 | Basics.v, Induction.v (帰納法による証明) | スライド |
演習問題(締切 10/29 10:30: Basics.v の plus_id_exercise, mult_S_1, zero_nbeq_plus_1, Induction.v の basic_induction, double_plus, beq_nat_refl)，次週の予習 |
| 4 | 10/29 | 単純型付ラムダ計算 | 資料 | 次週の予習 |
| 5 | 11/5 | 単純型付ラムダ計算(型付け), Lists.v | スライド |
演習問題(締切 11/12 10:30: Lists.v の fst_swap_is_snd, list_funs, list_exercises, beq_natlist)，次週の予習
|
| 6 | 11/12 | Lists.v の残り, Poly.v | スライド |
演習問題(締切 11/19 10:30: Lists.v の hd_opt, Poly.v の split, poly_exercises, partition, flat_map)，次週の予習 |
| 7 | 11/19 | System F, MoreCoq.v 前半 | 資料, スライド | |
| 8 | 11/26 | MoreCoq.v 後半 | |
演習問題(締切 12/3 10:30: MoreCoq.v の silly_ex, sillyex1, sillyex2, plus_n_n_injective, beq_nat_true, gen_dep_practice, override_shadow, destruct_eqn_practice) |
| 9 | 12/3 | 自然演繹と Coq | 資料 | 次週の予習 |
| 10 | 12/10 | 命題論理とカリー・ハワード同型対応 | 資料 | |
| 11 | 12/17 | Logic.v | スライド | 演習問題(締切 1/7 10:30: Logic.v の and_assoc, iff_properties, or_distributes_over_and_2, contrapositive,
not_both_true_and_false, false_beq_nat)
|
| 12 | 1/7 | Prop.v | スライド | 演習問題(締切 1/14 10:30: Prop.v の
double_even, ev_sum, b_times2, gorgeous_plus13, gorgeous_sum, inversion_practice) |
| 13 | 1/14 | MoreLogic.v (前半) | スライド | 演習問題 (締切 1/21 10:30: MoreLogic.v の dist_not_exist, dist_exists_or) |
| 14 | 1/21 | 演習 | 問題集 | |
| 15 | 1/28 | 演習 | | |
| 期末試験 | 2/4 | | | |