「ソフトウェア基礎論」講義計画佐藤、亀山 - Programming Logic Group

プログラム理論特論
２００２年１学期
亀山幸義
筑波大学
システム情報工学研究科
コンピュータサイエンス専攻
本講義の位置付け

プログラム理論(プログラム言語の理論)の基
礎を学ぶ．
×プログラムをどううまく作るか
○プログラムがどうしてうまく動いているのか
○正しく動くプログラムとは何か
○どうやってプログラムの正しさを保証するのか
○どうやって正しいプログラムを作るか
○どうやって(正しさを保ちつつ)効率良いプログ
ラムに変換するのか
講義の目的

「型システム」と「論理」を keyword と
したプログラム理論の研究分野の一端を
紹介する．
型システムとはなにか
型があると何がよいのか
型と論理の関係は？
型システムの応用は？
講義計画

プログラム言語の基礎理論
プログラム言語における型システム
 関数プログラミングとラムダ計算
 型つきラムダ計算
 型理論の基礎
 型理論の応用


セキュリティ、プログラム解析
スケジュール
講義：4/11, 18, 25,
5/9, 16, 23, 30,
6/6, 13, 20
 試験：6/27

講義資料の置き場所

ホームページ:
http://logic.is.tsukuba.ac.jp/
~kam/progtheory/
参考書

S. Thompson, “Type Theory and Functional
Programming”, Addison-Wesley, 1991.
萩谷昌己「ソフトウェア科学のための論理学」，
岩波講座ソフトウェア科学１１，岩波書店
 佐藤雅彦，桜井貴文「プログラムの基礎理
論」，岩波講座ソフトウェア科学１３，岩波書
店


Download Report