A-031 コンパイラ構築の証明論的枠組み(モデル・アルゴリズム・プログラミング,一般論文)

情報処理学会

書誌事項

タイトル別名
  • A-031 A Proof Theoretical Framework for Compiler Construction

この論文をさがす

抄録

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

収録刊行物

詳細情報 詳細情報について

問題の指摘

ページトップへ