We have a prove that the type-system used in mira, to debug register allocation settings is sound. This means that we have proofs of progress and preservation. By the way, Twelf is fun! One should give it a try, because proving theorems in twelf is just like playing video-games: its is a very interactive process, and quite exciting (after surpassed the initial horror for logical relations:). We really thank the twelf team for the wonderful job, in particular Daniel Lee, for the handy help. Also we thank Todd Millstein and Daniel Marino for the invaluable help in understanding type theory and the techniques of mechanical proofs.

Last update:
March 26^{th}, 2007.