Changeset 1740 for Deliverables
- Timestamp:
- Feb 24, 2012, 2:32:04 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1739 r1740 66 66 \end{center} 67 67 68 Here, by `endo-transformation', we mean a mapping from language back to itself: 69 the loop optimization step maps the Clight language to itself. 70 68 71 %Our overall statements of correctness with respect to costs will 69 72 %require a correctly labelled program 70 71 73 There are three layers in most of the proofs proposed: 72 74 \begin{enumerate} … … 275 277 \end{center} 276 278 277 Here, by `endo-transformation', we mean a mapping from language back to itself.278 For example, the constant propagation step maps the RTL language to the RTL language.279 280 279 \subsection{The RTLabs to RTL translation} 281 280 \label{subsect.rtlabs.rtl.translation}
Note: See TracChangeset
for help on using the changeset viewer.