Top > Search Research paper > (In Japanese)性能に関して健全なコンパイラの構築に向けて

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

Research report code R030000276
Posted date Feb 22, 2005
Researchers
  • (In Japanese)南出 靖彦
Affiliation
  • (In Japanese)筑波大学電子・情報工学系
Research organization
  • (In Japanese)筑波大学
Report name (In Japanese)性能に関して健全なコンパイラの構築に向けて
Technology summary (In Japanese)プログラムが期待したように動作することを保証するためには、ソース・プログラムからわかるプログラムの実行時間、メモリーの使用状況などプログラムの性能に関連した様々な性質が、実行コードでも成り立つ必要がある。そこで、本研究では、プログラムの性能を理論的に扱い、性能を考慮した上で期待したように動作する実行コードを生成するコンパイラを構築できるようにする。そのために、まず、プログラムの性能を理論的に議論するためのプログラミング言語の意味論を確立する。その上で、コンパイラで用いられる様々なプログラム変換が、性能に関して期待される性質を満たしていることを厳密に証明していく。また、コンパイラの性質の証明を厳密に行う場合には、その証明は非常に複雑かつ冗長なものになり、今度は、その証明自体の正しさを確認することが非常に困難になると思われる。そこで、本研究では、プログラム変換の正当性をより確実に示すために、証明をコンピュータのプログラムとして実現されている定理証明システムで行い、証明の検証を行うことも目指す。
Research field
  • System programmings in general
  • Operating systems
  • Language processors
  • General‐purpose programming language
Published papers related (In Japanese)(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.
Research project
  • Precursory Research for Embryonic Science and Technology.;Information and Human Activity
Information research report
  • (In Japanese)南出 靖彦. 性能に関して健全なコンパイラの構築に向けて. 「さきがけ研究21」研究報告会 「情報と知」領域 講演要旨集 第III期研究者(研究期間:1999-2002),2002. p.21 - 26.

PAGE TOP