@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}}
}