Soundness Proofs

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.

Download it 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.
Download it arith.elf: Types of numbers: zero and successor of number. From the example given by Brigitte Pientka.
Download it list.elf: Types of lists, with projection and update operations.
Download it os_smira.elf: The operational semantics of the smira language.
Download it tp_smira.elf: Types of the smira language.
Download it 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.
Download it smira.thm: The proofs of progress and preservation for our smira type-system.

Last update: March 26th, 2007.