Ignore:
Timestamp:
Apr 29, 2013, 6:14:15 PM (6 years ago)
Author:
tranquil
Message:

summary for D4.4, and other modifications

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2637 r3213  
    12641264\bibliography{ccexec}
    12651265
    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 16-th 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 re-compile 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.237-252.
    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 Bi-Directional 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.
     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 16-th 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 re-compile 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.237-252.
     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 Bi-Directional 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.
    12981298
    12991299\end{document}
Note: See TracChangeset for help on using the changeset viewer.