A certifying compiler for Java

This paper presents the initial results of a project to determine if the te chniques of proof-carrying code and certifying compilers can be applied to programming languages of realistic size and complexity. The experiment show s that: (1) it is possible to implement a certifying native-code compiler f or a large subset of the Java programming language; (2) the compiler is fre ely able to apply many standard local and global optimizations; and (3) the PCC binaries it produces are of reasonable size and can be rapidly checked for type safety by a small proof-checker. This paper also presents further evidence that PCC provides several advantages for compiler development. In particular, generating proofs of the target code helps to identify compile r bugs, many of which would have been difficult to discover by testing.