TOP > 研究報告検索 > 性能に関して健全なコンパイラの構築に向けて

性能に関して健全なコンパイラの構築に向けて

研究報告コード R030000276
掲載日 2005年2月22日
研究者
  • 南出 靖彦
研究者所属機関
  • 筑波大学電子・情報工学系
研究機関
  • 筑波大学
報告名称 性能に関して健全なコンパイラの構築に向けて
報告概要 プログラムが期待したように動作することを保証するためには、ソース・プログラムからわかるプログラムの実行時間、メモリーの使用状況などプログラムの性能に関連した様々な性質が、実行コードでも成り立つ必要がある。そこで、本研究では、プログラムの性能を理論的に扱い、性能を考慮した上で期待したように動作する実行コードを生成するコンパイラを構築できるようにする。そのために、まず、プログラムの性能を理論的に議論するためのプログラミング言語の意味論を確立する。その上で、コンパイラで用いられる様々なプログラム変換が、性能に関して期待される性質を満たしていることを厳密に証明していく。また、コンパイラの性質の証明を厳密に行う場合には、その証明は非常に複雑かつ冗長なものになり、今度は、その証明自体の正しさを確認することが非常に困難になると思われる。そこで、本研究では、プログラム変換の正当性をより確実に示すために、証明をコンピュータのプログラムとして実現されている定理証明システムで行い、証明の検証を行うことも目指す。
研究分野
  • システムプログラミング一般
  • オペレーティングシステム
  • 言語プロセッサ
  • 汎用プログラミング言語
関連発表論文 (1) 大熊浩示,南出靖彦,定理証明システムを用いたCPS変換の正当性の検証,ソフトウェア科学会第17回大会, 2000.
(2) Yasuhiko Minamide, A New Criterion for Safe Program Transformations, In Proceedings of the Forth International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), ENTCS 41, 2000.
(3) Yasuhiko Minamide, Runtime Behavior of Conversion Interpretation of Subtyping, In Proceedings of the 13th International Workshop on the Implementation of Functional Languages, LNCS 2312, pages 155-167, 2001.
(4). Yasuhiko Minamide, Selective Tail Call Elimination, In Proceedings of the 14th International Workshop on Implementation of Functional Languages, 2002.
研究制度
  • さきがけ研究21 「情報と知」領域
研究報告資料
  • 南出 靖彦. 性能に関して健全なコンパイラの構築に向けて. 「さきがけ研究21」研究報告会 「情報と知」領域 講演要旨集 第III期研究者(研究期間:1999-2002),2002. p.21 - 26.

PAGE TOP