Changeset 3249


Ignore:
Timestamp:
May 1, 2013, 1:54:59 AM (4 years ago)
Author:
stark
Message:

UEDIN D3.4, D6.4-6.5

Location:
Deliverables
Files:
2 added
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3236 r3249  
    102102
    103103
    104 \cerco{} Work Package 3, \emph{Verified Compiler - front end} aims
    105 for formalise and verify the front-end of the \cerco{} cost lifting
    106 compiler.  This document accompanies the final deliverable,
    107 \textbf{D3.4: Front-end Correctness Proofs}.  The deliverable consists
    108 of the formal correctness proofs for the front-end, written in the
    109 \matita{} proof assistant and this document provides report on the
    110 work carried out for it.
     104This document reports on \textbf{D3.4:~Front-end Correctness Proofs}, the
     105final deliverable of \cerco{} work package~3 \emph{Verified Compiler - front
     106  end}.  That work package was devoted to the formalisation and verification of
     107the front-end of the \cerco{} cost lifting compiler, and Deliverable~3.4 is a
     108machine-checked formal correctness proof of the compiler front-end, written in
     109the \matita{} proof assistant.
     110
     111The proof itself is contained in a series of Matita files, listed in
     112Appendix~A and culminating in the lemma \lstinline'front_end_correct' and the
     113theorem \lstinline'correct' in the file \lstinline'correctness.ma'.  This
     114document accompanies the deliverable and briefly reports on the work carried
     115out in the development of that proof.
    111116
    112117\vspace*{1cm}
     
    802807we consider is an $8$-bit one. In \textsf{Clight}, casts are
    803808expressions. Hence, most of the work of this transformation
    804 proceeds on expressions. The tranformation proceeds by recursively
     809proceeds on expressions. The transformation proceeds by recursively
    805810trying to coerce an expression to a particular integer type, which
    806811is in practice smaller than the original one. This functionality
Note: See TracChangeset for help on using the changeset viewer.