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

some changes

Location:
Deliverables/D4.1/ITP-Paper
Files:
2 edited

Legend:

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

    r814 r815  
    7373
    7474@inproceedings
     75{ blanqui:designing:2010,
     76  title = {Designing a {CPU} model: from a pseudo-formal document to fast code},
     77  author = {Fr\'ed\'eric Blanqui and Claude Helmstetter and Vania Joloboff and Jean-Fran\c{c}ois Monin and Xiaomu Shi},
     78  booktitle = {Proceedings of the $\mathrm{3^{rd}}$ Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools},
     79  year = {2010}
     80}
     81
     82@inproceedings
    7583{ blazy:formal:2006,
    7684  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
  • 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.