Abstract |
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} }
Last modified: Thu Jul 30 10:55:26 CEST 2009 |