最適化の検証を行うコンパイラのための型システム(サイバー増大号)

概要

論文の詳細を見る
This paper presents a type theoretical framework for the verification of compiler optimizations. Although today's compiler optimizations are fairly advanced, there is still not an appropriate theoretical framework for the verification of compiler optimizations. To establish a generalized theoretical framework, we introduce assignment types for variables that represent how the value of variables will be calculated in a program. In this paper, first we introduce our type system. Second we prove soundness of our type system. This implies that the given two programs are equivalent if their return values are equal in types. Soundness ensures that many structure preserving optimizations preserve program semantics. Furthermore, by extending the notion of type equality to order relations, we redefine several optimizations and prove that they also preserve program semantics.
2005-07-26