ソフトウェア論理

ソフトウェア論理
Instructor(s)	亀山幸義、水谷哲也
E-Mail	亀山:　kam、水谷:　mizutani (それぞれの後に @cs.tsukuba.ac.jpをつけること）
URL	http://logic.cs.tsukuba.ac.jp/~kam/lics/
Office hours	授業の始めに連絡する。
Cource#	01CH201
Area	知能ソフトウェア
Course style	講義
Term	秋AB
Period	火5,6
Room#	3B303
Outline	論理は、ソフトウェア科学の様々な面に現れ大きな役割を果たしている。この講義では、ソフトウェア科学における論理の役割について、 (1) プログラム言語の意味論と型システム、 (2) プログラムの仕様記述と検証の論理、の2つの側面から考察する。
Keywords	Symbolic Logic, Type System, Lambda Calculus, Specification, Verification, Semantics, Hoare Logic, Temporal Logic.
Prerequisites	必須ではないが、命題論理とプログラム言語の基礎的事項を理解していると講義を理解しやすい。
Course plan	亀山担当分では、型システムを中心としたプログラム言語の基礎理論を解説する。具体的な題材は以下の通りである。ラムダ計算とプログラム言語プログラム言語の形式と意味型システムと直観主義論理発展的な話題：継続渡し方式など水谷担当分では、プログラムの仕様記述と検証技法について解説する。具体的な題材は以下の通りである。逐次型プログラムの検証: ホーア論理並列プログラムの仕様記述および検証: 時相論理 (temporal logic) 実時間プログラムの仕様記述および検証: 時間を陽に扱う理論
Textbook	必要に応じて、講義の際に資料を配付する。
References	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.
Evaluation	講義への出席を前提として、レポートまたは演習により成績を評価する。期末試験は行わない。
TF / TA