A provably sound TAL for back-end optimization

Typed assembly languages provide a way to generate machinecheckable safety proofs for machine-language programs. But the soundness proofs of most existing typed assembly languages are hand-written and cannot be machine-checked, which is worrisome for such large calculi. We have designed and implemented a low-level typed assembly language (LTAL) with a semantic model and established its soundness from the model. Compared to existing typed assembly languages, LTAL is more scalable and more secure; it has no macro instructions that hinder low-level optimizations such as instruction scheduling; its type constructors are expressive enough to capture dataflow information, support the compiler’s choice of data representations and permit typed position-independent code; and its type-checking algorithm is completely syntax-directed. We have built a prototype system, based on Standard ML of New Jersey, that compiles most of core ML to Sparc code. We explain how we were able to make the untyp...

• Type: Conference
• Year: 2003
• Where: PLDI
• Authors: Juan Chen, Dinghao Wu, Andrew W. Appel, Hai Fang
• Keywords: Low-level Optimizations, Low-level Typed Assembly, PLDI 2003, Programming Languages, Typed Assembly Language