Changeset 1728 for Deliverables


Ignore:
Timestamp:
Feb 23, 2012, 1:48:20 PM (8 years ago)
Author:
mulligan
Message:

avoiding conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1727 r1728  
    3535\section{Introduction}
    3636\label{sect.introduction}
     37
     38In the last project review of the CerCo project, the project reviewers expressed the opinion that it would be a good idea to attempt to write down some of the statements of the correctness theorems that we intend to prove about the complexity preserving compiler.
     39This document provides a very high-level, pen-and-paper sketch of what we view as the best path to completing the correctness proof for the compiler.
     40In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof.
    3741
    3842\section{The RTLabs to RTL translation}
Note: See TracChangeset for help on using the changeset viewer.