Inferring annotated types for inter-procedural register allocation with constructor flattening

We introduce an annotated type system for a compiler intermediate language. The type system is designed to support inter-procedural register allocation and the representation of tuples and variants directly in the register file. We present an algorithm that generates constraints for assigning annotations, and prove its soundness with respect to the type system. Categories and Subject Descriptors D.3.4 [Programming Languages]: Processors—compilers General Terms Languages, Reliability, Verification Keywords Type Systems, Effects, Register Allocation, Defunctionalization, Certifying Compilers

• Type: Conference
• Year: 2003
• Where: TLDI
• Authors: Torben Amtoft, Robert Muller
• Keywords: Formal Methods, Inter-procedural Register Allocation, Register Allocation, TLDI 2003, Type Systems