A Type System for Verification of Compiler Optimizations

概要

論文の詳細を見る
This paper presents a type theoretical framework for the verification of compiler optimizations. Though 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 framework, we introduce assignment types for variables, which represent how the value of variables will be calculated in a program. First we introduce our type system. Second we prove soundness of our type system meaning that if types of return values are equal in two programs, the programs are equivalent. Soundness ensures that many structure preserving optimizations preserve program semantics. Then by extending the notion of type equality to order relation, we redefine several optimizations and prove that they also preserve program semantics.
一般社団法人情報処理学会の論文
2004-07-15