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

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

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

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

本講義をもとにした教科書の出版に伴い，配布資料の公開を終了いたしました．(2011.7.15)
配布資料(11)～(13)を置きました (2011.1.27)
最終レポート課題を 1/18 の講義で出しました．(2011.1.27)．
テキスト第10章を置きました (2011.1.10)
テキスト第8～9章を置きました (2010.12.6)
テキスト第5～7章を置きました (2010.11.26)
演習システムの使い方の資料とテキスト第3～4章を置きました (2010.11.2)
レポート課題を出しました (2010.10.29)
- レポート課題: 配布資料の定理2.4の証明を完成させよ．
- 提出形式: 紙
- 締切: 11/9(火) 13:00(授業開始時)
LaTeX で導出木を書いてみたいという猛者には国立情報学研究所龍田真教授が開発したマクロ(proof.sty)がオススメです．
配布資料(0)とテキスト第1～2章を置きました (2010.10.5)
今年度のページ立ち上げ (2010.9.2)

演習システムの評価はスコアによる相対評価でしょうか。それとも一問50/150点による評価でしょうか。: 絶対評価ですが，1問1/3点にするかどうかは答えません．
レポート課題は５０点を問題数で割り振る形式でしょうか。例えば二つ解いたら一問あたり25点、といったぐあいでしょうか。: まあそんな感じですかね．どれを選んだから配点が高い，とか，そういうことはありません．(もちろん，書けばなんとでもなるような課題は質も求めますが．)
ノートをとっていなかったため、講義で証明されたメタ定理がどれだか忘れてしまったのですが、基本的にテキストで証明してある定理以外を証明すれば大丈夫でしょうか。: 基本的にはそうです．中間レポートの問題はもちろん除きます．

date	講義内容(予定)	配布資料
10/5	事務連絡；導入；自然数の加算・乗算・比較と導出システム(1)	配布資料(0), テキスト第1～2章
10/12	自然数の加算・乗算・比較と導出システム(2)
10/19	(出張により休講予定)
10/26	メタ定理と帰納法による証明(1)
11/2	演習	演習システムの使い方
11/9	メタ定理と帰納法による証明(2), 整数・真偽値式の評価	テキスト第3～4章
11/16	整数・真偽値式の評価，定義・変数束縛と環境
11/23	(勤労感謝の日)
11/30	定義・変数束縛と環境，関数と再帰	テキスト第5～7章
12/7	関数と再帰，静的有効範囲と名前無し表現	テキスト第8～9章
12/14	静的有効範囲と名前無し表現，リストとパターンマッチング
12/21	型システム(1)
1/11	型システム(2)	テキスト第10章
1/18	型推論
1/25	(第一級)継続	配布資料(11)，配布資料(12)
2/1	参照	配布資料(13)

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:: 2011-07-15 10:00:57 +0900#$