Explicitly Typed Static Single-Assignment Form
Static single-assignment form (SSA) is an important optimizing compiler intermediate representation, and is widely used in many real-world production compilers, such as GCC, LLVM, Jikes, and MLton, etc.. This paper presents the initial results of our project to apply the techniques of proof-carrying code and certifying compilation to practical highlyoptimizing compilers. To be specific, this paper presents the design of an explicitly typed static single-assignment form called TSSA. This paper presents a formalization of TSSA by defining its abstract syntax, the operational semantics, and the static semantics. This paper leads to a general semantics foundation for SSA-based optimizing compilers.
static single-assignment form type system
Baojian Hua BoXu Ying Gao
School of Software Engineering,, & Suzhou Institute for Advanced Study University of Science and Tec School of Software Engineering University of Science and Technology of China Hefei,China Intel China Research Center Beijing,China
国际会议
上海
英文
43-47
2010-06-22（万方平台首次上网日期，不代表论文的发表时间）