- 05/13/11 18:07:36 (2 years ago)
- 1 modified
r802 r803 106 106 \item The reviewers suggest to quickly outline pencil-and-paper 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 to 111 experiment different proof strategies w ere possible. In particular, we will 112 try to exploit dependent types in our formali zation. Dependent types were 111 We plan to since we want to 112 experiment different proof strategies were possible. In particular, we will 113 try to exploit dependent types in our formaliependent 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 compiler 115 started to formali 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 ation. 119 120 120 \item The reviewers suggest touse this estimation to compare two possible 121 \item The reviewers suggest 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 re-use the CompCert proofs.