2026-05-15T04:00:53Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00016672 2025-01-22T23:44:26Z 934:935:959:961

A Type System for Verification of Compiler Optimizations A Type System for Verification of Compiler Optimizations YUTAKA, MATSUNO HIROYUKI, SATO Yutaka, Matsuno Hiroyuki, Sato 通常論文 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. 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. journal article 情報処理学会 2004-07-15 application/pdf 情報処理学会論文誌プログラミング（PRO） SIG09(PRO22) 45 14 24 1882-7802 AA11464814 https://ipsj.ixsq.nii.ac.jp/record/16672/files/IPSJ-TPRO4509003.pdf eng