|
ソフトウェア論理
|
|
| 担当教員 |
亀山幸義、水谷哲也
|
| 電子メール | 亀山: kam、水谷: mizutani (それぞれの後に @cs.tsukuba.ac.jpをつけること） |
| URL | http://logic.cs.tsukuba.ac.jp/~kam/lics/ |
| オフィスアワー | 授業の始めに連絡する。 |
| 科目番号 | 01CH201 |
| 分野 | 知能ソフトウェア |
| 授業形態 | 講義 |
| 学期 | 秋AB |
| 時限 | 金5,6 |
| 教室 | 3B303 |
| 授業概要 | 論理は、ソフトウェア科学の様々な面に現れ大きな役割 を果たしている。この講義では、ソフトウェア科学にお ける論理の役割について、 (1) プログラム言語の意味 論と型システム、 (2) プログラムの仕様記述と検証の 論理、の2つの側面から考察する。 |
| キーワード | 記号論理、型システム、ラムダ計算、意味論、仕様記述、検 証、 ホーア論理、時相論理。 |
| Keyword | Symbolic Logic, Type System, Lambda Calculus, Specification, Verification, Semantics, Hoare Logic, Temporal Logic. |
| 予備知識 | 必須ではないが、命題論理とプログラム言語 の基礎的事項を理解していると講義を理解しやすい。 |
| 授業内容 |
亀山担当分では、
型システムを中心としたプログラム言語の基礎理論を解
説する。
具体的な題材は以下の通りである。
|
| 教科書 | 必要に応じて、講義の際に資料を配付する。 |
| 参考書 |
B. C. Pierce, "Types and Programming Languages",
MIT Press, 2002. M. Huth and M. Ryan, "Logic in Computer Science (Second Edition)", Cambridge Univ. Press, 2004. |
| 成績評価 | 講義への出席を前提として、レポートまたは演習により成績を 評価する。期末試験は行わない。 |
| TF・TA | |