Ignore:
Timestamp:
May 19, 2011, 12:24:48 PM (9 years ago)
Author:
mulligan
Message:

some changes

File:
1 edited

Legend:

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

    r814 r815  
    786786Perhaps the closest project to CerCo is CompCert~\cite{leroy:formally:2009}.
    787787CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC.
    788 (Coq and Matita essentially share the same logic.)
     788The CompCert C compiler is extracted to O'Caml using Coq's code extraction facility.
     789We aim to make use of a similar facility in Matita.
     790Many other formalised emulators/compilers have also been extracted from proof assistants using similar technology (e.g. see~\cite{blanqui:designing:2010}).
    789791
    790792Despite this similarity, the two formalisations do not have much in common.
Note: See TracChangeset for help on using the changeset viewer.