Changeset 3213 for Papers/itp2013
 Timestamp:
 Apr 29, 2013, 6:14:15 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2637 r3213 1264 1264 \bibliography{ccexec} 1265 1265 1266 \appendix1267 \section{Notes for the reviewers}1268 1269 The results described in the paper are part of a larger formalization1270 (the certification of the CerCo compiler). At the moment of the submission1271 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 the1273 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 the1275 formalization described here. At the moment a rough approximation suggests1276 about 2700 lines of Matita code.1277 1278 We will also attach the development version of the interactive theorem1279 prover Matita that compiles the submitted formalization. Another possibility1280 is to backport the development to the last released version of the system1281 to avoid having to recompile Matita from scratch.1282 1283 The programming and certification style used in the formalization heavily1284 exploit dependent types. Dependent types are used: 1) to impose invariants1285 by construction on the data types and operations (e.g. a traces from a state1286 $s_1$ to a state $s_2$ can be concatenad to a trace from a state1287 $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 of1289 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 depends1291 mandatorily on dependent types: it should be easy to adapt the technique1292 and results presented in the paper to HOL.1293 1294 Finally, Matita and Coq are based on minor variations of the Calculus of1295 (Co)Inductive Constructions. These variations do not affect the CerCo1296 formalization. Therefore a porting of the proofs and ideas to Coq would be1297 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 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 1298 1299 1299 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.