# Changeset 3249

Ignore:
Timestamp:
May 1, 2013, 1:54:59 AM (5 years ago)
Message:

UEDIN D3.4, D6.4-6.5

Location:
Deliverables
Files:
 r3236 \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} 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