Changeset 2637 for Papers

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


1 edited


  • Papers/itp-2013/ccexec.tex

    r2635 r2637  
     1267\section{Notes for the reviewers}
     1269The results described in the paper are part of a larger formalization
     1270(the certification of the CerCo compiler). At the moment of the submission
     1271we need to single out from the CerCo formalization the results presented here.
     1272Before the 16-th of February we will submit an attachment that contains the
     1273minimal subset of the CerCo formalization that allows to prove those results.
     1274At that time it will also be possible to measure exactly the size of the
     1275formalization described here. At the moment a rough approximation suggests
     1276about 2700 lines of Matita code.
     1278We will also attach the development version of the interactive theorem
     1279prover Matita that compiles the submitted formalization. Another possibility
     1280is to backport the development to the last released version of the system
     1281to avoid having to re-compile Matita from scratch.
     1283The programming and certification style used in the formalization heavily
     1284exploit dependent types. Dependent types are used: 1) to impose invariants
     1285by 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)
     1288to state and prove the theorems by using the Russell methodology of
     1289Matthieu 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
     1291mandatorily on dependent types: it should be easy to adapt the technique
     1292and results presented in the paper to HOL.
     1294Finally, Matita and Coq are based on minor variations of the Calculus of
     1295(Co)Inductive Constructions. These variations do not affect the CerCo
     1296formalization. Therefore a porting of the proofs and ideas to Coq would be
     1297rather straightforward.
Note: See TracChangeset for help on using the changeset viewer.