知能情報学専攻ソフトウェア基礎論 (2011年度冬学期)

日時	火曜日3限(13:00～14:30)
場所	工学部10号館4階第二講義室

講義内容(シラバスより)

数理論理学的手法を用いたソフトウェア科学の基礎理論について講述する．特に、プログラミング言語の形式化と意味論、また，型システムとプログラムの安全性など，形式化を用いたプログラムの性質に関する議論をする．

お知らせ

1/31 の講義に関する配布資料を置きました．(2012.01.29)
最終レポート課題を出しました．(2012.1.17)
12/20 の講義では第8章の残りと第9章をカバーします．(2011.12.14)
12/6 は演習です．12/13 の講義では，第8章をカバーします．(2011.11.29)
11/22 の講義は教科書第5，6章をカバーします．(2011.11.15)

レポート課題を出しました．(2011.11.8)

締切	11/15 13:00
提出方法	pdf(手書きスキャンも可)を講義のメールアドレスへ
課題	教科書定理2.2～2.27 のいずれかを証明すること．ただし，教科書・講義で取り上げていないものに限る．定理2.11～2.13 については導出システムをひとつ選べばよい．定理2.14 については，(1)～(3) の同値性証明のうち一部でよい．
注意	帰納法を用いる際は，何についての帰納法か明記し，述語 P が何であるかを明記すること．

11/15 の講義は教科書の第３章，第４章を読んでいることを前提として行います．(2011.11.8)
11/1 の講義は教科書の第２章を読んでいることを前提として行います．(2011.10.18)
10/25 の引き続き演習です．(2011.10.18)
10/11の講義は教科書第1章を読んでいることを前提とします．(2011.10.4)
今年度のページ立ち上げ (2011.9.2)

講義スケジュールと配布資料

date	講義内容(予定)	配布資料
10/4	事務連絡；導入；自然数の加算・乗算・比較と導出システム(1)
10/11	自然数の加算・乗算・比較と導出システム(2)
10/18	算術式の評価と簡約; 演習
10/25	演習
11/1	メタ定理と帰納法による証明(1)
11/8	メタ定理と帰納法による証明(2)
11/15	整数・真偽値式の評価 / 定義，変数束縛と環境
11/22	関数と再帰
11/29	静的有効範囲と名前無し表現 / リストとパターンマッチング
12/6	演習
12/13	型システム(1)
12/20	型システム(2)
1/17	型推論
1/24	(演習)
1/31	継続と参照	継続, 第一級継続, 参照
2/7	(補講？)
2/14	最終レポート締切 (予定)

教科書

五十嵐淳. プログラミング言語の基礎概念. サイエンス社. 2011.

参考図書

Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
Daniel P. Friedman and Mitchell Wand. Essentials of Programming Languages. The MIT Press. Third edition. 2008.

igarashi@kuis.kyoto-u.ac.jp

Last update on $Date:: 2012-01-29 23:40:47 +0900#$