# Changeset 1740

Ignore:
Timestamp:
Feb 24, 2012, 2:32:04 PM (7 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r1739 \end{center} Here, by endo-transformation', we mean a mapping from language back to itself: the loop optimization step maps the Clight language to itself. %Our overall statements of correctness with respect to costs will %require a correctly labelled program There are three layers in most of the proofs proposed: \begin{enumerate} \end{center} Here, by endo-transformation', we mean a mapping from language back to itself. For example, the constant propagation step maps the RTL language to the RTL language. \subsection{The RTLabs to RTL translation} \label{subsect.rtlabs.rtl.translation}