• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

コード言語の最適化技術と検証技術を統合する証明システムの研究

研究課題

研究課題/領域番号 19500021
研究種目

基盤研究(C)

配分区分補助金
応募区分一般
研究分野 ソフトウエア
研究機関東北大学

研究代表者

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

研究期間 (年度) 2007 – 2008
研究課題ステータス 完了 (2008年度)
配分額 *注記
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2008年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2007年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
キーワードプログラミング言語 / コード最適化 / コード検証 / 証明論
研究概要

直観主義的論理学の自然演繹証明システムとラムダ計算との同型関係を拡張・一般化し, 機械語コードの証明論を完成し, コードの最適化やコードの検証をより体系的に行う基礎を構築した。この証明論では, 機械語コードは, 左規則のみからなるある種のシーケント計算として表現され, その操作的意味, すなわち, コードを実行する機械の状態遷移規則は, シーケント計算のカット除去定理の証明から系統的に抽出することができる。さらに, この証明システムは, 低レベルコードのアクセス権限の検証や制御フロー遷移の最適化などの基礎となることが示された。

報告書

(3件)
  • 2008 実績報告書   研究成果報告書 ( PDF )
  • 2007 実績報告書
  • 研究成果

    (4件)

すべて 2008 2007

すべて 雑誌論文 (4件) (うち査読あり 4件)

  • [雑誌論文] 型代入を遅延する最適化型推論アルゴリズム2008

    • 著者名/発表者名
      上野雄大, 大堀淳
    • 雑誌名

      コンピュータソフトウェア 25

      ページ: 101-113

    • NAID

      40022111605

    • 関連する報告書
      2008 研究成果報告書
    • 査読あり
  • [雑誌論文] 制御フローの合流のための計算系2008

    • 著者名/発表者名
      上野雄大, 大堀淳
    • 雑誌名

      情報処理学会論文誌プログラミング(PRO) 1

      ページ: 19-33

    • NAID

      110007970871

    • 関連する報告書
      2008 実績報告書 2008 研究成果報告書
    • 査読あり
  • [雑誌論文] 型代入を遅延する髄化型推論アルゴリズム2008

    • 著者名/発表者名
      上野雄大, 大堀淳
    • 雑誌名

      コンピュータソフトウェア 25

      ページ: 101-113

    • 関連する報告書
      2008 実績報告書
    • 査読あり
  • [雑誌論文] A Proof Theory for Machine Code2007

    • 著者名/発表者名
      Atsushi Ohori
    • 雑誌名

      ACM Transactions on Programming Languages and Systems 29(6)

    • 関連する報告書
      2008 研究成果報告書 2007 実績報告書
    • 査読あり

URL: 

公開日: 2007-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi