| 日時 | 火曜日3限(13:00〜14:30) |
| 場所 | 総合研究7号館1階 情報1 |
| オフィスアワー: | 月曜日 17:00〜18:30 (総合研究7号館224) |
| (その他の時間は要アポイントメント) |
| 締切 | 5/21(火) 13:00 |
|---|---|
| 提出方法 | pdf(手書きスキャンも可)を講義のメールアドレスへ． |
| 課題 | 教科書 定理2.2~2.27 のいずれかを証明すること．ただし， 教科書・講義で取り上げていないものに限る．定理2.11~2.13 については導出システム をひとつ選べばよい．定理2.14 については，(1)~(3) の同値性証明のうち一部でよい． |
| 注意 | 帰納法を用いる際は，何についての帰納法か明記し，述語 P が何であるかを明記すること． |
LaTeX で導出木を書いてみたいという猛者には国立情報学研究所龍田真教授が開発した マクロ(proof.sty)がオススメです．
| 回数 | date | 講義内容(予定)/配布資料 | |
|---|---|---|---|
| 1 | 4/9 | 事務連絡；導入；自然数の加算・乗算・比較と導出システム(1) (資料) | |
| 2 | 4/16 | 自然数の加算・乗算・比較と導出システム(2) | |
| 3 | 4/23 | 算術式の評価と簡約，メタ定理，演習 (資料) | |
| 4 | 4/30 | メタ定理と帰納法による証明 | |
| 5 | 5/7 | メタ定理と帰納法による証明 | |
| 6 | 5/14 | MLの操作的意味論(1): 整数・真偽値式の評価 | |
| 7 | 5/21 | MLの操作的意味論(2): 定義，変数束縛と環境 | |
| 8 | 5/28 | MLの操作的意味論(3): 関数と再帰 | |
| 9 | 6/4 | (演習) | |
| 10 | 6/11 | MLの操作的意味論(4): 静的有効範囲と名前無し表現 | |
| 11 | 6/25 | MLの操作的意味論(5): リストとパターンマッチ，型システム(1) | |
| 12 | 7/2 | (演習) | |
| 13 | 7/9 | 型システム(2) | |
| 14 | 7/16 | 多相型システム | |
| 15 | 7/23 | 型推論 |