Investigating Type-Certifying Compilation with Isabelle

This paper 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.
 

Online Copy

Available as PDF
 
 

Isabelle Sources

Available as gzip tar, awaiting integration into the Isabelle distribution...
 

BibTeX Entry

@InProceedings{strecker02:type_certif_compil,
  author =       {Martin Strecker},
  title =        {Investigating Type-Certifying Compilation with {Isabelle}},
  booktitle =    {Proc. Conference on Logic for Programming, 
                 Artificial Intelligence, and Reasoning (LPAR)},
  year =         2002,
  volume =       2514,
  series =       {Lecture Notes in Computer Science},
  publisher =    {Springer Verlag}
}