知能情報学専攻 ソフトウェア基礎論 (2008年度冬学期)
日時 | 火曜日3限(13:00〜14:30) |
場所 | 工学部10号館4階第二講義室 |
講義内容(シラバスより)
数理論理学的手法を用いたソフトウェア科学の基礎理論について講述する.特に、
プログラミング言語の形式化と意味論、また,型システムとプログラムの安全性な
ど,形式化を用いたプログラムの性質に関する議論をする.
お知らせ
- 本講義をもとにした教科書の出版に伴い,配布資料の公開を終了いたしました.(2011.7.15)
- 配布資料9を置きました.講義中の訂正は反映したものです.また,
配布資料7は欠番とします.(2009.1.27)
- 最終レポート課題を出題しました.締切は
2/12 です.(2009.1.13)
- 配布資料8を置きました.(2009.1.13)
- 演習システムに問題を追加しました.これで最後の追加です.(2009.1.9)
- 配布資料6(追補)を置きました.(2008.12.01)
- 演習システム(ML1以降)で,マイナスの後に空白を入れずに数字を書くと,
(OCaml と違い)負の数になってしまいますので注意して下さい.例えば,
f-1
は f
を -1
に適用する,とい
う意味になります.同様に ML1 では 1-1
は構文エラーになりま
す.(2008.12.01)
- 演習システムに問題を追加しました.(2008.11.20)
- 配布資料6を置きました.(2008.11.11)
- 配布資料4,5を置きました.(2008.11.04)
- 演習システムに問題を追加しました.(2008.11.04)
- 10/28は演習を行います.希望アカウント名を10/23(木)までに知らせてく
ださい.また当日は各自ノートPCを持参してください.事前にKUINS-IIIオープ
ンスペースからWebへアクセスできるように設定をしておいてください.(参考:
KUINS-III
利用ガイド集) (2008.10.21)
- 配布資料3,付録1を置きました.(2008.10.21)
- 配布資料2を置きました.(2008.10.17)
- 受講者は演習システムの希望アカウント名を講義用メイルアドレスまで送っ
てください.(講義直後の時点でアドレスが有効ではありませんでした.今は大
丈夫です.)(2008.10.07)
- 配布資料0と1を置きました.(2008.10.07)
- 今年度のページ立ち上げ (2008.8.26)
講義スケジュールと配布資料
date | 講義内容(予定) | 配布資料 |
10/7 | 事務連絡・導入 | resume0.pdf |
10/14 | 自然数の加算・乗算・比較と導出システム | resume1.pdf |
10/21 | 簡単な式の評価 | resume2.pdf |
10/28 | 演習 | app1.pdf |
11/4 | 変数束縛と関数 | resume3.pdf, resume4.pdf |
11/11 | リストとパターンマッチ | resume5.pdf |
11/18 | 単純型システム | resume6.pdf |
12/2 | 型安全性の証明 | resume6-2.pdf |
12/9 | A型インフルエンザのため休講 | |
12/16 | 型推論 | |
1/13 | 多相型システム | resume8.pdf |
1/20 | 出張につき休講 | |
1/27 | 多相型システムに対する型安全性定理・型推論 | resume9.pdf |
2/12(木) | 最終レポート締切 | |
参考図書
- 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.
- Robin Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.
igarashi@kuis.kyoto-u.ac.jp
Last update on $Date: $.