Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual
Machine code with types to enable a one-pass verification of welltypedness.
We have formalized a variant of their proposal in the theorem prover
Isabelle/HOL and proved soundness and completeness.
@article{KleinN-CCPE01,
author = {Gerwin Klein and Tobias Nipkow},
title = {Verified Lightweight Bytecode Verification},
journal = {Concurrency and Computation: Practice and Experience},
editor = {S. Eisenbach and G. T. Leavens},
publisher = {John Wiley and Sons},
volume = 13,
number = 13,
pages = {1133-1151},
year = 2001
url = {\url{http://www4.in.tum.de/~kleing/papers/cpe01.html}}