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

プログラム理論特論
２００３年１学期
亀山幸義 ([email protected])
筑波大学
システム情報工学研究科コンピュータサイエンス専攻
理工学研究科電子・情報工学分野
講義の目的

「型システム」（と「論理」）を
keyword としたプログラム理論の一端を
紹介する．
型システムとはなにか
型があると何がよいのか
型と論理の関係は？
型システムの応用は？
講義計画
1.
2.
3.
4.
5.
6.
7.
8.
9.
概要
プログラム言語における型システム
型つきラムダ計算
型検査と型推論
多相型
コントロールオペレータ
CPS変換
応用（Javaバイトコードの検証etc.)
まとめ
講義概要（つづき）
プログラム言語



本講義では C, Java, ML, Scheme を念頭に置く
特に、ML, Java （の一部)を切り出して例題に使う
型のないラムダ計算（λ計算）



関数型言語のおもちゃ
Schemeに対応
型付きラムダ計算



本講義で基礎として使う体系
基本的な事項は「計算論理」の講義資料を参照のこと
型検査と型推論



型検査‥プログラムと型が与えられたとき、型が整合しているか検
査すること
型推論‥プログラムが与えられたとき、整合的な型を見つけること
講義概要（つづき）
多相型






型変数を持つ型
map: （α→β)→(list(α)→list(β))
sort: (α→α→Bool)→（list(α)→list(α))
ML に含まれている
Java は？
コントロールオペレータ






Java, ML の例外（exception), C のsetjmp/longjmp
Scheme, ある種の ML の call/cc
Prolog の ! (cut operator)
純粋なラムダ計算には存在しないが、便利
まともな型システムの範囲におさまるのか？
CPS変換




CPS = Continuation Passing Style とはなにか？
コンパイラとの関係
型システムや論理とどう関係するのか？
講義概要（つづき）

応用：話題、回数とも未定（なくなる可能性も
あり）




CPS変換の続き（call-by-name, call-by-valueと
の関係）
Javaバイトコードの検証（２００２年度「プログラ
ム理論」の資料を参照）
型システムを用いたセキュリティ検証
情報流解析
スケジュール
講義：4/8, 15, 22,
5/6, 13, 20, 27,
6/3, 10, 17
途中１回前後休講の可能性あり
 レポート（２回)で採点、試験は行わない

参考書

S. Thompson, “Type Theory and Functional
Programming”, Addison-Wesley, 1991.
萩谷昌己「ソフトウェア科学のための論理学」，
岩波講座ソフトウェア科学１１，岩波書店
 佐藤雅彦，桜井貴文「プログラムの基礎理
論」，岩波講座ソフトウェア科学１３，岩波書
店

講義に関する情報源
web page
http://logic.is.tsukuba.ac.jp/
~kam/progtheory/
問合せ
[email protected]
3F809, 3E306

Download Report