| 研究概要 |
本研究の最終的な目的は,機械語コードの論理学的解釈を基礎とし,コードの利用や,最適化,検証などを統一的に行うことを可能にする系統的な枠組みを構築することである.特に,コードの最適化と検証を統一的に扱う論理学的枠組みの確立とそれに基づく最適化と検証技術の構築し,それによって,ラムダ計算の型理論が果たしたと同様に,低レベルコードに対しても,その安全性の検証やより効率的なコードへの最適化などを系統的に行うことを可能にする基礎理論の確立である.本年度は,この一般的な目的の基礎となる機械語コードの証明論を完成させた.この証明論の枠組みでは,機械語コードは直感主義的論理学の証明論の一つであるある種のシーケント計算系の証明とみなせ,機械語コードの実行はシーケント計算系のCut除去定理に対応する.この対応から,高水準言語からの機械語コードへのコンパイルは,自然演繹システムからこの証明システムへの証明変換として系統的に与えられ,さらに,機械語コードに対応する証明を自然演繹システムの証明に変換することによって,機械語コードを,ソース言語を参照することなしに,高水準言語に変換する可能性が与えられる.これら結果は,コードの最適化やコードの検証の論理学的な基礎を与えるものである.これら結果の一部は,論文A. Ohori, A Proof System for Machine Code, ACM Transactions on Programming Languages and Systems (ACM TOPLAS), vol29, no6. 2007に発表された.ACM TOPLASはプログラミング言語の分野で最も権威と影響力のある雑誌である.
|
