Changeset 803 for Deliverables
 Timestamp:
 May 13, 2011, 6:07:36 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/addenda/letter.tex
r802 r803 106 106 \item The reviewers suggest to quickly outline pencilandpaper correctness 107 107 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. 109 110 110 We plan to perform the proof departing from CompCertsince we want to111 experiment different proof strategies w ere possible. In particular, we will112 try to exploit dependent types in our formali zation. Dependent types were111 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 113 114 avoided as a design principle in CompCert. For this reason, we have already 114 started to formali ze in Matita the intermediate languages of our compiler115 started to formalise in Matita the intermediate languages of our compiler, 115 116 recording invariants in the types themselves and rearranging some code. 116 117 This should be completed at month 18. At this point we will be able to 117 118 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. 119 120 120 \item The reviewers suggest touse this estimation to compare two possible121 \item The reviewers suggest we use this estimation to compare two possible 121 122 scenarios: a) proceed as planned, porting all CompCert proofs to Matita or 122 123 b) port D3.1 and D4.1 to Coq and reuse the CompCert proofs.
Note: See TracChangeset
for help on using the changeset viewer.