Compiler Verification for C0

This paper describes formalisations of a type-safe fragment of the C programming language (called C0) and of the DLX assembly language. It then presents the definition and correctness proof of a substantial fragment of a C0-to-DLX compiler, carried out in the proof assistant Isabelle.
 

Online Copy

Available as PDF
 

BibTeX Entry

@TechReport{strecker05:_compil_verif_c0,
  author = 	 {Martin Strecker},
  title = 	 {Compiler Verification for {C0} (intermediate report)},
  institution =  {Universit{\'e} Paul Sabatier},
  year = 	 2005,
  address =	 {Toulouse},
  month =	 {April}
}