Index: /Deliverables/D4.1/ITP-Paper/itp-2011.tex
===================================================================
--- /Deliverables/D4.1/ITP-Paper/itp-2011.tex (revision 562)
+++ /Deliverables/D4.1/ITP-Paper/itp-2011.tex (revision 563)
@@ -754,6 +754,6 @@
In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably.
-Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009}.
-CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM.
+Perhaps the closest project to CerCo is CompCert~\cite{leroy:formally:2009}.
+CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC.
Coq and Matita essentially share the same logic.