Changeset 3249 for Deliverables/D3.4
- Timestamp:
- May 1, 2013, 1:54:59 AM (8 years ago)
- Location:
- Deliverables/D3.4/Report
- Files:
-
- 1 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 front-end of the \cerco{} cost lifting 106 compiler. This document accompanies the final deliverable, 107 \textbf{D3.4: Front-end Correctness Proofs}. The deliverable consists 108 of the formal correctness proofs for the front-end, 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:~Front-end 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 front-end of the \cerco{} cost lifting compiler, and Deliverable~3.4 is a 108 machine-checked formal correctness proof of the compiler front-end, 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.