| 研究概要 |
本研究では,ヘテロジニアスな環境におけるソフトウェア構築を容易にする環境適応型ソフトウェアを提案し,そのようなソフトウェアの意味論と,安全性向上のための型理論などの基礎理論を研究してきた.本年度の成果は以下の通り.
プログラム特化の安全性確保のための型理論構築
論理の証明体系と計算体系の間の一般的な同型対応を利用して,線形時間時相論理の証明体系からプログラム特化を行う多段階計算のための型付計算体系を構築し,その型理論による体系の安全性などを証明した.また,そのような計算体系に基づく,簡単なプログラミング言語を設計するとともに,実装方式として抽象機械とその機械語へのコンパイル技法を研究し,予備的な結果を得た.
明示的環境・メタ変数に関する意味論の研究
実行時メタ情報を抽象化した明示的環境を取り入れた計算体系の意味論研究に取り組み,強正規化性(停止性)という計算体系の重要な性質を保つ範囲で,よりきめ細かな環境特化の制御を行うことが可能な計算体系を構築するという成果をあげた.
継続に関する意味論・型理論の研究
実行制御に関するメタ情報を抽象化した継続に関する意味論・型理論の研究を行い,継続を第一級の値として扱うための言語機構である階層型shift/resetを使うプログラムの安全性確保のための型システムや,停止性の一般的な証明技法を構築するなどの成果をあげた.
|
