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 |