Verifying Compiler

A branch that attempts to prove the correctness of a compiler, and that any program a compiler tries to program is Type Safe.