著者
大堀 淳
出版者
FIT(電子情報通信学会・情報処理学会)運営委員会
雑誌
情報科学技術フォーラム講演論文集
巻号頁・発行日
vol.8, no.1, pp.319-320, 2009-08-20

本発表では,コンパイラを系統的に構築することを可能にする証明論的な枠組みを提案する.本枠組みでは,ソース言語,ターゲットの機械語言語,さらにコンパイル段階に現れる中間言語は,すべて,論理学の証明システムとして表現され,コンパイルの各段階は,それら証明システム間の証明変換として表現される.さらに,それら証明システム間の証明変換は,証明システムのカット除関係を保存することを示すことができる.この表明論的枠組みは構成的であり,証明システム間の変換が可能であると言う性質の証明から,対応するコンパイル段階を実現するアルゴリズムが抽出できる.このアルゴリズムは,その構成方法から,型と操作的意味を保存することが帰結する.