Changeset 802


Ignore:
Timestamp:
May 13, 2011, 5:55:43 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/addenda/letter.tex

    r801 r802  
    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.
     108 estimation of the complexity and time required to complete the formalization.
     109
     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
     113 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 recording invariants in the types themselves and rearranging some code.
     116 This should be completed at month 18. At this point we will be able to
     117 correctly state the intermediate proof statements and to estimate the
     118 complexity and effort for the formalization.
     119
     120\item The reviewers suggest to use this estimation to compare two possible
     121 scenarios: a) proceed as planned, porting all CompCert proofs to Matita or
     122 b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.
     123
     124
    109125
    110126\end{enumerate}
    111127
    112 
    113 Deliverable~6.2, the \emph{Plan for the Use and Dissemination of Foreground}
    114 was submitted as the first report of the {\cerco} project.  Following the
    115 scientific review of the project at the end of its first year, the reviewers
    116 recommended preparation of an addendum to specifically list future
    117 dissemination plans.  This is that addendum.
    118128\end{document}
    119129
Note: See TracChangeset for help on using the changeset viewer.