This article presents a type certifying compiler for a subset of Java and proves the type correctness of the bytecode it generates in the proof assistant Isabelle. The proof is performed by defining a type compiler that emits a type certificate and by showing a correspondence between bytecode and the certificate which entails well-typing. The basis for this work is an extensive formalization of the Java bytecode type system, which is first presented in an abstract, lattice-theoretic setting and then instantiated to Java types.

@article{KleinS-JLP04,
  author =  {Gerwin Klein and Martin Strecker},
  title =   {Verified {B}ytecode {V}erification and Type-Certifying {C}ompilation},
  journal = {Journal of Logic and Algebraic Programming},
  volume =  58,
  number =  {1--2},
  pages =   {27--60},
  year =    2004,
  url =     {\url{http://www4.in.tum.de/~kleing/papers/jlp02.html}}
}