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 highly-optimizing 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.