Changeset 3249 for Deliverables/D3.4

Timestamp:

May 1, 2013, 1:54:59 AM (7 years ago)

Author:

Ian Stark

Message:

UEDIN D3.4, D6.4-6.5

Location:

Deliverables/D3.4/Report

Files:

• report.pdf (added)
• report.tex (modified) (2 diffs)

Deliverables/D3.4/Report/report.tex

@@ -102 +102 @@
 
 
-\cerco{} Work Package 3, \emph{Verified Compiler - front end} aims
-for formalise and verify the front-end of the \cerco{} cost lifting
-compiler.  This document accompanies the final deliverable,
-\textbf{D3.4: Front-end Correctness Proofs}.  The deliverable consists
-of the formal correctness proofs for the front-end, written in the
-\matita{} proof assistant and this document provides report on the
-work carried out for it.
+This document reports on \textbf{D3.4:~Front-end Correctness Proofs}, the
+final deliverable of \cerco{} work package~3 \emph{Verified Compiler - front
+  end}.  That work package was devoted to the formalisation and verification of
+the front-end of the \cerco{} cost lifting compiler, and Deliverable~3.4 is a
+machine-checked formal correctness proof of the compiler front-end, written in
+the \matita{} proof assistant.
+
+The proof itself is contained in a series of Matita files, listed in
+Appendix~A and culminating in the lemma \lstinline'front_end_correct' and the
+theorem \lstinline'correct' in the file \lstinline'correctness.ma'.  This
+document accompanies the deliverable and briefly reports on the work carried
+out in the development of that proof.
 
 \vspace*{1cm}
@@ -802 +807 @@
 we consider is an $8$-bit one. In \textsf{Clight}, casts are 
 expressions. Hence, most of the work of this transformation 
-proceeds on expressions. The tranformation proceeds by recursively 
+proceeds on expressions. The transformation proceeds by recursively 
 trying to coerce an expression to a particular integer type, which 
 is in practice smaller than the original one. This functionality