Changeset 803

Timestamp:

05/13/11 18:07:36 (2 years ago)

Author:

mulligan

Message:

more changes

Files:

• 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 of the complexity and time required to complete the formalization.
+ estimation for the complexity of completing the formalisation, and time required
+ to do so.
 
- 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
+ We plan to depart from CompCert when carrying out our proof since we want to
+ experiment different proof strategies where possible. In particular, we will
+ try to exploit dependent types in our formalisation, as 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
+ started to formalise 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.
+ complexity and effort needed for the formalisation.
 
-\item The reviewers suggest to use this estimation to compare two possible
+\item The reviewers suggest we 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.