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.
|
|
The complete proof is in this zip file. You can load it in your twelf environment, and if the world hasn't changed too much since March 26th, 2007, you probably will get an [OK] from the twelf server :) By the way, this zip contains all the files needed, but if you only want to read the proof, you can browse through the files below. |
|
|
arith.elf: Types of numbers: zero and successor of number. From the example given by Brigitte Pientka. |
|
|
list.elf: Types of lists, with projection and update operations. |
|
|
os_smira.elf: The operational semantics of the smira language. |
|
|
tp_smira.elf: Types of the smira language. |
|
|
sub.thm: Theorems proved about subtyping. We have opted to define subtyping in an algorithm way. Thus, all the lemmas, including transitivity of the subtyping relationship are proved by induction on lists. |
|
|
smira.thm: The proofs of progress and preservation for our smira type-system. |