システム情報研究科　コンピュータサイエンス専攻　科目一覧　- シラバス -

ソフトウェア論理_E
担当教員	Yukiyoshi Kameyama, Tetsuya Mizutani
電子メール	Kameyama: kam (AT) cs.tsukuba.ac.jp, Mizutani: mizutani (AT) cs.tsukuba.ac.jp
URL	http://logic.cs.tsukuba.ac.jp/~kam/lics/
オフィスアワー	Office hours will be announced at the first lecture.
科目番号	01CH201
分野	Intelligent Software
授業形態	Lecture
学期	FallAB
時限	Fri5,6
教室	3B303
授業概要	Logic plays an important role in the study of software science. In this course, we study two important aspects of the role of logic in computer software; (1) logic and semantics of programming languages, and (2) logic for specification and verification of programs.
キーワード
Keyword	Symbolic Logic, Type System, Lambda Calculus, Specification, Verification, Semantics, Hoare Logic, Temporal Logic.
予備知識	Familiarity with propositional/predicate calculi (logic) and fundamentals of programming languages will be helpful, though not necessary.
授業内容	The course is divided into two parts, corresponding to each lecturer. One half is devoted to the foundational study of programming languages based on types systems. Lambda calculus and programming language. Semantics of programming languages. Type system and intuitionistic logic. Continuation passing style. The other half is devoted to the formal specification and verification of programs. Hoare Logic for sequential programs. Temporal logic for parallel programs. Some new theories for real-timing programs.
教科書	Handouts will be distributed at the lecture.
参考書	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.
成績評価	On the basis of (1) attendance to the lectures, and (2) the scores of reports and in-class exercises. No examination.
TF・TA