# Changeset 2637 for Papers/itp-2013/ccexec.tex

Ignore:
Timestamp:
Feb 6, 2013, 11:51:35 PM (6 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2635 \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}