• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2010 Fiscal Year Annual Research Report

証明論に基づくコンパイラの系統的な構築法の研究

Research Project

Project/Area Number 22500023
Research InstitutionTohoku University

Principal Investigator

大堀 淳  東北大学, 電気通信研究所, 教授 (60252532)

Co-Investigator(Kenkyū-buntansha) 上野 雄大  東北大学, 電気通信研究所, 助教 (60551554)
森畑 明昌  東北大学, 電気通信研究所, 助教 (10582257)
Keywordsコンパイラ / 証明論 / 最適化 / プログラミング言語処理系
Research Abstract

平成22年度の研究計画の主なものは以下の3点であった.
(A)コンパイルの各中間言語の操作的意味に正確に対応するカット除去システムの定義
具体的には,「コード証明」,「値証明」,「環境証明」,「トップレベル証明」の各概念を,自然演繹システム及びシーケント計算それぞれに導入し,各証明システムを再定義し,さらに,その証明系に対し,カット除去定理を証明することを試みることを計画した.
(B)各証明変換の再定義及びその正しさの証明
具体的には,前項の操作的意味論に正確に対応するカット除去定理の結果を用いて,自然演繹システムからシーケント計算への証明変換がカット除去に関する性質を保存することを示し,証明変換によって抽出されるコンパイルアルゴリズムの正しさ(total correctness)を確立することの2点であった.
(C)実装技術および、最適化理論の研究
(A)に関しては,コンパイラの主要なコンポーネントの一つであるA正規形変換に対してこの目標をほぼ完全に達成し,さらにそれに対して(B)のカット除去の性質の保存定理を証明しることに成功した.(C)に関しては,本研究等の成果を基礎として開発を行っているSML#コンパイラのA-正規化変換の実装に,本研究の一部の結果を試験的に応用し,コンパイラの開発に応用可能であるとの知見を得た.さらに,SML#でのプログラム開発の過程で,本研究における証明論的な考え方に基づき,アプリケーションに特化したコンパイルのための証明論的拡張が可能であること,さらにそれら拡張はゲームプログラムの構築に有望であるとの萌芽的な洞察を得た.

  • Research Products

    (3 results)

All 2011 Other

All Presentation (2 results) Remarks (1 results)

  • [Presentation] 宣言的記述からの関数型言語によるゲームプログラムの導出2011

    • Author(s)
      松島勇介, 上野雄大, 森畑明昌, 大堀淳
    • Organizer
      第13回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      札幌市
    • Year and Date
      2011-03-10
  • [Presentation] 生存区間を変数名とする中間表現の実装と,それに基づく最適化2011

    • Author(s)
      高橋和将, 森畑明昌, 上野雄大, 大堀淳
    • Organizer
      第13回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      札幌市
    • Year and Date
      2011-03-09
  • [Remarks]

    • URL

      http://www.pllab.riec.tohoku.ac.jp/

URL: 

Published: 2013-06-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi