Abstract |
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.
Online Copy |
Available as PDF
Isabelle Sources |
Available as gzip tar, awaiting
integration into the Isabelle distribution...
BibTeX Entry |
@Article{klein04:_formal_compil_bytec_verif, author = {Gerwin Klein and Martin Strecker}, title = {Verified Bytecode Verification and Type-Certifying Compilation}, journal = {The Journal of Logic and Algebraic Programming}, year = 2004, volume = 58, pages = {27-60} }
Last modified: Thu Jul 30 10:54:42 CEST 2009 |