Changeset 1795 for Deliverables/D1.2/CompilerProofOutline/outline.tex

Timestamp:

Feb 28, 2012, 6:11:32 PM (8 years ago)

Author:

sacerdot

Message:

Final version, waiting for comments.

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (1 diff)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -118 +118 @@
 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 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.
-
-Finally, in the last section we present an estimation of the effort required for the certification in Matita of the compiler and draw conclusions.
+We also attach the draft for a paper that describes in more details the
+certification of the optimizing assembler. 
+
+Finally, 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.
 
 \section{Front-end: Clight to RTLabs}