Changeset 563 for Deliverables


Ignore:
Timestamp:
Feb 17, 2011, 4:45:17 PM (11 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r562 r563  
    754754In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably.
    755755
    756 Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009}.
    757 CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM.
     756Perhaps the closest project to CerCo is CompCert~\cite{leroy:formally:2009}.
     757CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC.
    758758Coq and Matita essentially share the same logic.
    759759
Note: See TracChangeset for help on using the changeset viewer.