Changeset 803


Ignore:
Timestamp:
May 13, 2011, 6:07:36 PM (9 years ago)
Author:
mulligan
Message:

more changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/addenda/letter.tex

    r802 r803  
    106106\item The reviewers suggest to quickly outline pencil-and-paper correctness
    107107 proofs for each of the seven stages of the compiler in order to establish an
    108  estimation of the complexity and time required to complete the formalization.
     108 estimation for the complexity of completing the formalisation, and time required
     109 to do so.
    109110
    110  We plan to perform the proof departing from CompCert since we want to
    111  experiment different proof strategies were possible. In particular, we will
    112  try to exploit dependent types in our formalization. Dependent types were
     111 We plan to depart from CompCert when carrying out our proof since we want to
     112 experiment different proof strategies where possible. In particular, we will
     113 try to exploit dependent types in our formalisation, as dependent types were
    113114 avoided as a design principle in CompCert. For this reason, we have already
    114  started to formalize in Matita the intermediate languages of our compiler
     115 started to formalise in Matita the intermediate languages of our compiler,
    115116 recording invariants in the types themselves and rearranging some code.
    116117 This should be completed at month 18. At this point we will be able to
    117118 correctly state the intermediate proof statements and to estimate the
    118  complexity and effort for the formalization.
     119 complexity and effort needed for the formalisation.
    119120
    120 \item The reviewers suggest to use this estimation to compare two possible
     121\item The reviewers suggest we use this estimation to compare two possible
    121122 scenarios: a) proceed as planned, porting all CompCert proofs to Matita or
    122123 b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.
Note: See TracChangeset for help on using the changeset viewer.