 Timestamp:
 Feb 6, 2013, 11:51:35 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2635 r2637 1264 1264 \bibliography{ccexec} 1265 1265 1266 \appendix 1267 \section{Notes for the reviewers} 1268 1269 The results described in the paper are part of a larger formalization 1270 (the certification of the CerCo compiler). At the moment of the submission 1271 we need to single out from the CerCo formalization the results presented here. 1272 Before the 16th of February we will submit an attachment that contains the 1273 minimal subset of the CerCo formalization that allows to prove those results. 1274 At that time it will also be possible to measure exactly the size of the 1275 formalization described here. At the moment a rough approximation suggests 1276 about 2700 lines of Matita code. 1277 1278 We will also attach the development version of the interactive theorem 1279 prover Matita that compiles the submitted formalization. Another possibility 1280 is to backport the development to the last released version of the system 1281 to avoid having to recompile Matita from scratch. 1282 1283 The programming and certification style used in the formalization heavily 1284 exploit dependent types. Dependent types are used: 1) to impose invariants 1285 by construction on the data types and operations (e.g. a traces from a state 1286 $s_1$ to a state $s_2$ can be concatenad to a trace from a state 1287 $s_2'$ to a state $s_3$ only if $s_2$ is convertible with $s_2'$); 2) 1288 to state and prove the theorems by using the Russell methodology of 1289 Matthieu Sozeau\footnote{Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237252. 1290 }, better known in the Coq world as ``\texttt{Program}'' and reimplemented in a simpler way in Matita using coercion propagations\footnote{Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi: A BiDirectional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science 8(1) (2012)}. However, no result presented depends 1291 mandatorily on dependent types: it should be easy to adapt the technique 1292 and results presented in the paper to HOL. 1293 1294 Finally, Matita and Coq are based on minor variations of the Calculus of 1295 (Co)Inductive Constructions. These variations do not affect the CerCo 1296 formalization. Therefore a porting of the proofs and ideas to Coq would be 1297 rather straightforward. 1298 1266 1299 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.