A type system for proving correctness of compiler optimizations is proposed. We introduce assignment types for variables, which abstract the calculation process of the value. Soundness of our type system ensures that if types of return values are equal in two programs, the programs are equivalent. Then by extending the notion of type equality to order relation, we redefine several optimizations and prove that they preserve program semantics.

Back to technical programme page