Changeset 1795 for Deliverables


Ignore:
Timestamp:
Feb 28, 2012, 6:11:32 PM (8 years ago)
Author:
sacerdot
Message:

Final version, waiting for comments.

File:
1 edited

Legend:

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

    r1794 r1795  
    118118In 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.
    119119We sketch the overall correctness results, and also briefly describe the parts of the proof that have already been completed at the end of the First Period.
    120 
    121 Finally, in the last section we present an estimation of the effort required for the certification in Matita of the compiler and draw conclusions.
     120We also attach the draft for a paper that describes in more details the
     121certification of the optimizing assembler.
     122
     123Finally, in the last sections before the attached paper we present an estimation of the effort required for the certification in Matita of the compiler and draw conclusions.
    122124
    123125\section{Front-end: Clight to RTLabs}
Note: See TracChangeset for help on using the changeset viewer.