Changeset 802 for Deliverables/addenda/letter.tex

Timestamp:

May 13, 2011, 5:55:43 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/addenda/letter.tex (modified) (1 diff)

Deliverables/addenda/letter.tex

@@ -106 +106 @@
 \item The reviewers suggest to quickly outline pencil-and-paper correctness
  proofs for each of the seven stages of the compiler in order to establish an
- estimation.
+ estimation of the complexity and time required to complete the formalization.
+
+ We plan to perform the proof departing from CompCert since we want to
+ experiment different proof strategies were possible. In particular, we will
+ try to exploit dependent types in our formalization. Dependent types were
+ avoided as a design principle in CompCert. For this reason, we have already
+ started to formalize in Matita the intermediate languages of our compiler
+ recording invariants in the types themselves and rearranging some code.
+ This should be completed at month 18. At this point we will be able to
+ correctly state the intermediate proof statements and to estimate the
+ complexity and effort for the formalization.
+
+\item The reviewers suggest to use this estimation to compare two possible
+ scenarios: a) proceed as planned, porting all CompCert proofs to Matita or
+ b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.
+
+
 
 \end{enumerate}
 
-
-Deliverable~6.2, the \emph{Plan for the Use and Dissemination of Foreground}
-was submitted as the first report of the {\cerco} project.  Following the
-scientific review of the project at the end of its first year, the reviewers
-recommended preparation of an addendum to specifically list future
-dissemination plans.  This is that addendum.
 \end{document}