Changeset 3249 for Deliverables
 Timestamp:
 May 1, 2013, 1:54:59 AM (8 years ago)
 Location:
 Deliverables
 Files:

 2 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3236 r3249 102 102 103 103 104 \cerco{} Work Package 3, \emph{Verified Compiler  front end} aims 105 for formalise and verify the frontend of the \cerco{} cost lifting 106 compiler. This document accompanies the final deliverable, 107 \textbf{D3.4: Frontend Correctness Proofs}. The deliverable consists 108 of the formal correctness proofs for the frontend, written in the 109 \matita{} proof assistant and this document provides report on the 110 work carried out for it. 104 This document reports on \textbf{D3.4:~Frontend Correctness Proofs}, the 105 final deliverable of \cerco{} work package~3 \emph{Verified Compiler  front 106 end}. That work package was devoted to the formalisation and verification of 107 the frontend of the \cerco{} cost lifting compiler, and Deliverable~3.4 is a 108 machinechecked formal correctness proof of the compiler frontend, written in 109 the \matita{} proof assistant. 110 111 The proof itself is contained in a series of Matita files, listed in 112 Appendix~A and culminating in the lemma \lstinline'front_end_correct' and the 113 theorem \lstinline'correct' in the file \lstinline'correctness.ma'. This 114 document accompanies the deliverable and briefly reports on the work carried 115 out in the development of that proof. 111 116 112 117 \vspace*{1cm} … … 802 807 we consider is an $8$bit one. In \textsf{Clight}, casts are 803 808 expressions. Hence, most of the work of this transformation 804 proceeds on expressions. The tran formation proceeds by recursively809 proceeds on expressions. The transformation proceeds by recursively 805 810 trying to coerce an expression to a particular integer type, which 806 811 is in practice smaller than the original one. This functionality
Note: See TracChangeset
for help on using the changeset viewer.