Changeset 1749 for Deliverables


Ignore:
Timestamp:
Feb 24, 2012, 4:55:51 PM (8 years ago)
Author:
sacerdot
Message:

Rephrased introduction.

File:
1 edited

Legend:

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

    r1748 r1749  
    3737\label{sect.introduction}
    3838
    39 In 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.
    40 This 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.
    41 In 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.
     39In the last project review of the CerCo project, the project reviewers
     40recommended us to quickly outline a paper-and-pencil correctness proof
     41for each of the stages of the CerCo compiler in order to allow for an
     42estimation of the complexity and time required to complete the formalization
     43of the proof. This has been possible starting from month 18 when we have
     44completed the formalization in Matita of the datastructures and code of
     45the compiler.
     46
     47In this document we provide a very high-level, pen-and-paper
     48sketch of what we view as the best path to completing the correctness proof
     49for the compiler. In 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. We also briefly describe the parts of the proof that have already
     50been completed at the end of the First Period.
     51
     52In the last section we finally present an estimation of the effort required
     53for the certification in Matita of the compiler.
    4254
    4355\section{Front-end: Clight to RTLabs}
Note: See TracChangeset for help on using the changeset viewer.