"Verified bytecode verification and type-certifying compilation."

Gerwin Klein, Martin Strecker (2004)
a service of Schloss Dagstuhl - Leibniz Center for Informatics