プログラム
9月15日(月）
13:30-14:00 受付 14:00-15:30 線形時間時相論理モデル検査90分早分かり
- 講師： 萩谷昌己先生（東京大学）
- モデル検査とは，与えられた状態遷移系が与えられた時相論理式を満たすか どうかを判定する手続きのことである．時相論理には，大きく，分岐時間を 扱うものと線形時間を扱うものの二種類がある．PLTLやCTL*などの線形時間時 相論理は，状態遷移系の無限の実行経路に関する性質を記述するので，それら のモデル検査には，無限の実行経路の判定を行うωオートマトンの構成を必要 とする．本チュートリアルでは，PLTL の論理式からタブロー法によってωオー トマトンを構成する方法について，90分という短い時間内で，なるべく易しく 説明したい．
15:30-16:00 休憩 16:00-17:30 Objective Caml によるプログラミング
- 講師： Jacques Garrigue先生（京都大学）
- 多くのバグを排除できる強い型システムと簡潔な表現を許す関数と値の自由な 扱いはObjective Camlの魅力である。このチュートリアルではObjective Caml の型システムの様々な面を紹介した後、それを具体的なプログラミングに応用 する。型推論の基礎から始め、プログラムが 型を誘導するのと同様に、型が プログラムの構築を誘導することを見る。できるだけ関数型プログラミングの 初心者が理解できながら、経験の長いプログラマでも興味がもてるものにした い。
8:30-10:00 パラメトリック・ポリモルフィズム
- 講師： 長谷川立先生（東京大学）
- プログラミング言語はプログラミングのための道具だから, 理屈なんかいらな い, 便利ならばよいというのも考え方だが, あえて理屈を追求してみると結構 深い世界が広がっている. ここでは, 単純な言語である型付きラムダ計算に 焦点を絞って, その背後にある理屈を考えてみたい. それがパラメトリシティ 原理と呼ばれるものである. この原理を通して見ることで, 拡がる世界の一 端を紹介することが, 当講演の目標である.
10:00-10:30 休憩 10:30-12:00 ガーベジコレクション
- 講師： 近山隆先生（東京大学）
- ガーベジコレクション（GC）は、複雑なデータ構造を扱うソフトウェアにおい て、使用したメモリ領域を自動的に回収・再利用する技術である。記号処理言 語Lispと共に生まれ発展してきたGC技術は、Lispの諸技術を受けついだJavaの 普及とともに、急速に利用が広がっている。本講では、GCの役割と基本的な考 え方から説き起こし、効率的なGCの容易な実現のための諸手法について概説す る。なお、一般的なコンピュータのハードウェアおよびソフトウェアの知識は 前提とするが、LispやJavaなどの言語についての知識は前提とせずにお話しす る。