2004 Fiscal Year Annual Research Report
| Project/Area Number |
15700011
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
五十嵐 淳 京都大学, 情報学研究科, 講師 (40323456)
|
|---|
| Keywords | 様相論理 / メタプログラミング / 型システム / 直観主義 / 不干渉性 / 線形時間時相論理 |
|---|
| Research Abstract |
本研究の主な目的は,様々なプログラム解析を統一的に扱える枠組みを,様相論理という論理体系を元にして開発し,実際のプログラミング言語の解析のための型システムとして応用することにある.本年度は,以下のふたつの研究を主に行った.
●昨年度研究を行った,情報流解析と対応する様相論理体系と,DCCと呼ばれる一般的なプログラム解析の枠組との関係についての研究
DCCはAbadiらによる,情報流解析などを含む一般的なプログラム解析の枠組であり,lax logicと呼ばれる様相論理の一種を型システムとみなし,発展させている.しかしlax logicと我々の研究した様相論理に基づく型システムは少なくとも表面的にはかなり異なっている,これらの関連を研究し,DCCで型がつくプログラムは,我々の型システムで型がつくプログラムに変換することが可能であることがわかった.これにより,少なくとも我々の枠組が型付けのレベルではDCCを包含するものである,ということがわかった.
●メタプログラミング言語と呼ばれる,プログラム自身を操作の対象とすることができるプログラミング言語の時相論理に基づいた設計
メタプログラミングの一例として,コンパイラ生成器のようにプログラムを生成するプログラムがあげられる.このような段階的計算を記述するための型付言語を,線形離散時間時相論理に対する自然演繹証明システムを開発し,それを型システムとみなすことで,設計した.「次の時刻でAである」「現時刻以降常にAである」といった命題を型として解釈することで,「次の段階で計算されるコード」「現段階以降いつでも実行できるコード」といった概念を型システムで捉え,プログラム中でデータとして扱われるコードの安全性や汎用性を高めることに成功した.
|
