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

定理証明システムによる型システムとプログラム変換の検証

研究課題

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

若手研究(B)

配分区分補助金
研究分野 計算機科学
研究機関筑波大学

研究代表者

南出 靖彦  筑波大学, 電子・情報工学系, 講師 (50252531)

研究期間 (年度) 2001 – 2002
研究課題ステータス 完了 (2002年度)
配分額 *注記
2,000千円 (直接経費: 2,000千円)
2002年度: 1,000千円 (直接経費: 1,000千円)
2001年度: 1,000千円 (直接経費: 1,000千円)
キーワード定理証明システム / 型システム / プログラム変換 / 操作的意味論
研究概要

関数型プログラミング言語のコンパイラで用いられるCPS変換の定理証明システムIsabelle/HOLによる検証について二つの拡張を行った.まず,CPS変換がプログラムの実行に必要な記憶領域の大きさを保存することを検証した.証明すべき性質はより複雑なものになり,証明の長さも2倍程度になった.しかし,変換で導入される変数の形式化などは,記憶領域を考慮しない場合の形式化をそのまま応用することができ,自動証明を多くの補題の証明に用いることができた.次に,変換の検証を自由変数に含む式に拡張した.前年度の検証では,扱うプログラムが閉じた式であることを仮定し,証明を単純化した.しかし,前年度の証明を再検討したところ,この制限は証明の単純化にあまり貢献していないことがわかった.そこで,本年度には,この制限を取り除いて検証を行い,この制限が本質的でないことを確認した.
関数型プログラミング言語の末尾呼び出しを,Java仮想機械などの末尾呼び出しを直接サポートしていない環境で効率的に実装するためのプログラム変換を提案した.末尾呼び出しをサポートしない環境でも,特殊な関数呼び出しの仕組みを用いることで,末尾呼び出しが実現できるが,そのような方法はオーバーヘッドが大きい.提案した方法では,型推論を用いてプログラムの末尾呼び出しに関する性質を推論する.その型情報に基づき,末尾呼び出しの正当な実装が必要な関数に対してだけ,選択的に,非効率的な末尾呼び出しの実装を用いることで,オーバーヘッドを抑えている.

報告書

(2件)
  • 2002 実績報告書
  • 2001 実績報告書
  • 研究成果

    (2件)

すべて その他

すべて 文献書誌 (2件)

  • [文献書誌] Yasuhiko Minamide, Koji Okuma: "Verifying the CPS transformation in Isabelle/HOL"Asian Workshop on Programming Languages and Systems. 29-37 (2001)

    • 関連する報告書
      2002 実績報告書
  • [文献書誌] Yasuhiko Minamide: "Runtime Behavior of Conversion Interpretation of Subtyping"Proceedings of International Workshop on Implementation of Functional Languages,Lecture Notes in Computer Science. (印刷中). (2001)

    • 関連する報告書
      2001 実績報告書

URL: 

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

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

Powered by NII kakenhi