2003 Fiscal Year Annual Research Report
プログラム解析のための統一型理論の構築・検証とそれに基づく解析器の自動合成
| Project/Area Number |
14702063
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
小林 直樹 東京工業大学, 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Keywords | 型システム / プログラム解析 / 定理証明支援器 / Coq / プログラム抽出 / 構成的プログラミング |
|---|
| Research Abstract |
近年,プログラム解析の最も有望な手法の一つとして型理論に基づく手法が注目されている.本研究では,プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し,さらにそれに基づき,構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.
1.プログラム解析のための統一的型理論の拡張・改良
種々のプログラム解析を統一的に扱うための型システムとして,これまで研究してきたメモリやファィル,ネットワークなど計算機資源へのアクセス方法を統一的に解析するための型システムの拡張,改良を行った.また,統一的型システムのさらなる拡張の必要性を探るため,これまでの理論では扱えない,順序付き線形型システムについて研究を行い,プログラム変換への応用を示した.
2.型理論に基づくプログラム解析器の抽出実験
正しいプログラム解析器を自動抽出するためめ実験として,昨年に引き続き,一部をパラメータ化した汎用的型システムライブラリの定理証明支援器Coq上での定式化を続けるとともに,その上に単純型付きラムダ計算の定式化をおこなって,汎用ライブラリの有効性を確かめた.
3.並行計算モデルの定理証明器上での定式化
並行プログラムのための統一的型システムの定式化の前準備として,並行計算モデルであるπ計算の構文および操作的意味,仕様を記述するためのプロセス論理のCoq上での定式化を昨年度に引き続き行った.
|
-
[Publications] Atsushi Igarashi, Naoki Kobayashi: "Resource Usage Analysis"ACM Transactions on Programming Languages and Systems. (出版予定). (2004)
-
[Publications] Atsushi Igarashi, Naoki Kobayashi: "A Generic Type System for the Pi-Calculus"Theoretical Computer Science. 311・1-3. 121-163 (2004)
-
[Publications] R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security - Theories and Systems, Springer LNCS. 2609. 217-233 (2003)
-
[Publications] Naoki Kobayashi: "Useless Code Elimination and Program Slicing for the Pi-Calculus"Proceedings of APLAS'03,Springer LNCS. 2895. 55-72 (2003)
-
[Publications] 児玉 紘一, 小林 直樹, 末永 幸平: "順序付き線形型に基づく木構造処理プログラムからストリーム処理プログラムへの変換"PPL2004論文集. 134-149 (2004)
