User loginNavigation 
Register Allocation by Proof TransformationRegister Allocation by Proof Transformation, Atsushi Ohori. ESOP 2003.
The idea that making uses of the structural rules explicit gives you proof terms to model registermemory moves is very pretty. Another fun thing to do would be to take a continuation calculus and apply the ideas here to see if it produces a good lowlevel IR. EDIT: Ehud asked for some further exposition, so here goes. At a high level, you can think of the need to do register allocation as arising from a mismatch between a programming language and the hardware. In a language, we refer to data using variables, and in any given expression, we can use as many variables as we like. However, when a CPU does stuff, it wants the data to be in registers  and it has only a small, finite set of them. So when a program is compiled, some variables can be represented by registers, and the rest must be represented by locations in memory (usually on the stack). Whenever the CPU needs to use a variable in memory, there must be explicit code to move it from memory into a register. The idea in this paper is to take the typing derivation of a program with an unbounded variable set, and then divide the context into two parts, one representing the register file and the other representing variables in memory. In terms of the implementation, moves between these two zones correspond to registermemory moves; and in terms of logic, this is a use of the structural rule of Exchange, which permutes the order of variables in a context. So this gives us a highlevel, machineindependent characterization of the register allocation problem: take a onezone derivation and convert it to a twozone derivation. But it gets even better: as long as the register allocation algorithm only adds uses of the structural rules in its transformation, we know that the meaning of the original program is unchanged  so this method also yields a simple way of proving that a register allocation pass is semanticspreserving. (The fact that this is an easy proof is one indication of the power of this idea.) By neelk at 20080411 22:08  Implementation  Lambda Calculus  Type Theory  other blogs  7289 reads

Browse archivesActive forum topics 
Recent comments
3 hours 59 min ago
3 hours 59 min ago
4 hours 11 min ago
10 hours 17 min ago
10 hours 54 min ago
11 hours 1 min ago
14 hours 8 min ago
16 hours 52 min ago
18 hours 10 min ago
18 hours 47 min ago