ソフトウェア論理 (Logic in Computer Software)

筑波大学システム情報工学研究科コンピュータサイエンス専攻
担当: 亀山幸義、水谷哲也
教室: 3B203 (受講人数によっては変更する可能性があります)

このページには、2012年度筑波大学大学院の授業『ソフトウェア論理』の資料を置きます。2011年度の資料はこちらです。

連絡事項

11月1日は休講です。(2012/10/25)
遅くなりましたが、10月18日の資料を置きました。(2012/10/25)
このページを作成。 (2012/03/25)

目次

シラバス日本語版，シラバス英語版
前半の講義計画 (担当：水谷哲也)
水谷先生の資料は、こちらのページにあります。
内容は、 Hoare Logic、@カリュキュラスなどに基づくプログラムの検証です。
後半の講義計画 (担当：亀山幸義)
- 第1週(10/18): 概要，ラムダ計算と不動点意味論
- 第2週(10/25): 型システム、マルチステージプログラミングスライド
- 11/1は休講です。
- 第3週(11/8): マルチステージプログラムの信頼性スライド
- 第4週(11/15): マルチステージプログラミングの応用スライド
後半の参考書
- Benjamine C. Pierce, "Types and Programming Languages", MIT Press, 2002.
- 大堀淳, プログラミング言語の基礎理論, 情報数学講座９，共立出版．
- 龍田真, 型理論, 近代科学社

亀山幸義 (ｋａｍ＃, 総合研究棟Ｂ 1008号室)
水谷哲也 (ｍｉｚｕｔａｎｉ＃, Ｅ棟 102号室)
上記の＃の部分は、＠ｃｓ．ｔｓｕｋｕｂａ．ａｃ．ｊｐで置き換えてください。