| With the growth of the Internet and of the use of computers in general, the safety and reliability of computer systems has taken much more importance. As the most popular methods to address these needs, such as discipline, authentication, or monitoring, are proving insufficient, there grows a need for formal methods that enable automatic verification of the safety of computer programs.; While approaches like model checking or Hoare logic hold the promise of proving not just safety but even correctness, their applicability is too restricted for general purpose applications. At the other end of the scale, type systems are very popular but only check a very limited set of properties and impose sometimes severe restrictions which can prevent some forms of optimizations and even whole categories of code.; In order to use type systems to guarantee the security of computer systems, applications need to ship with type annotations, which requires type-preserving compilers, i.e. compilers that preserve the source program's types at every stage of the compilation. As the program gets turned into lower level code, the restrictions imposed by the type system become more crippling, or alternatively, the type system needs to become more sophisticated.; My thesis defines and uses, within the context of type-preserving compilation, novel type systems for the purpose of proving more sophisticated properties of programs, thus trying to reduce the gap between program verification techniques and type systems. More specifically, I first present my experience porting the optimizer of the SML/NJ compiler to a type-preserving intermediate language. Then I extend this with a cross-module inliner and show a typed two-level language that allows me to formalize the inlining algorithm as a form of partial evaluation. In the second part, I develop techniques to type check a garbage collector and its interaction with the mutator. This leads me to develop a novel type system that allows me to reason about sophisticated invariants, much like Hoare logic would but without losing the modularity so crucial to the success of type systems. |
