@inbook{4a6c410f32324d3faffb078de63b779f,

title = "Register allocation by proof transformation",

abstract = "This paper presents a proof-theoretical framework that accounts for the entire process of register allocation - liveness analysis is proof reconstruction (similar to type inference), and register allocation is proof transformation from a proof system with unrestricted variable accesses to a proof system with restricted variable access. In our framework, the set of registers acts as a {"}working set{"} of the live variables at each instruction step, which changes during the execution of the code. This eliminates the ad-hoc notion of {"}spilling{"}. The necessary memory-register moves are systematically incorporated in our proof transformation process. Its correctness is a direct corollary of our construction; the resulting proof is equivalent to the proof of the original code modulo treatment of structural rules. The framework yields a clean and powerful register allocation algorithm. The algorithm has been implemented, demonstrating the feasibility of the framework.",

author = "Atsushi Ohori",

year = "2003",

doi = "10.1007/3-540-36575-3_27",

language = "English",

isbn = "3540008861",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "399--413",

editor = "Pierpaolo Degano",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}