Investigating Type-Certifying Compilation with Isabelle

Martin Strecker



 
 Abstract

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


Last modified: Sat Nov 11 20:37:10 CET 2006