Changeset 2637

Timestamp:

Feb 6, 2013, 11:51:35 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Papers/itp-2013/ccexec.tex (modified) (1 diff)

Papers/itp-2013/ccexec.tex

@@ -1264 +1264 @@
 \bibliography{ccexec}
 
+\appendix
+\section{Notes for the reviewers}
+
+The results described in the paper are part of a larger formalization
+(the certification of the CerCo compiler). At the moment of the submission
+we need to single out from the CerCo formalization the results presented here.
+Before the 16-th of February we will submit an attachment that contains the
+minimal subset of the CerCo formalization that allows to prove those results.
+At that time it will also be possible to measure exactly the size of the
+formalization described here. At the moment a rough approximation suggests
+about 2700 lines of Matita code.
+
+We will also attach the development version of the interactive theorem
+prover Matita that compiles the submitted formalization. Another possibility
+is to backport the development to the last released version of the system
+to avoid having to re-compile Matita from scratch.
+
+The programming and certification style used in the formalization heavily
+exploit dependent types. Dependent types are used: 1) to impose invariants
+by construction on the data types and operations (e.g. a traces from a state
+$s_1$ to a state $s_2$ can be concatenad to a trace from a state
+$s_2'$ to a state $s_3$ only if $s_2$ is convertible with $s_2'$); 2)
+to state and prove the theorems by using the Russell methodology of
+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.
+}, 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
+mandatorily on dependent types: it should be easy to adapt the technique
+and results presented in the paper to HOL.
+
+Finally, Matita and Coq are based on minor variations of the Calculus of
+(Co)Inductive Constructions. These variations do not affect the CerCo
+formalization. Therefore a porting of the proofs and ideas to Coq would be
+rather straightforward.
+
 \end{document}