出版社：Information and Media Technologies Editorial Board
摘要：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.
关键词：theoretical framework for compiler optimizations;type system;recursive types;def-use analysis;SSA form
