MAJ release 1.6

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1224 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 5 insertions, 8 deletions

diff --git a/doc/index.html b/doc/index.html
index 88151d1..3c7337b 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,11 +24,11 @@ a:active {color : Red; text-decoration : underline; }
 
 <H1 align="center">The Compcert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 1.5, 2009-08-28</H3>
+<H3 align="center">Version 1.6, 2010-01-12</H3>
 
 <H2>Introduction</H2>
 
-<P>Compcert is a compiler that generates PowerPC assembly
+<P>Compcert is a compiler that generates PowerPC and ARM assembly
 code from Clight, a large subset of the C programming language.
 The particularity of this compiler is that it is written mostly within
 the specification language of the Coq proof assistant, and its
@@ -40,15 +40,12 @@ within the Coq proof assistant.</P>
 correctness can be found in the following papers (in increasing order of technical details):</P>
 <UL>
 <LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
-<LI>Xavier Leroy, <A
-HREF="http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf">Formal
-certification of a compiler back-end, or: programming a compiler with
-a proof assistant</A>.  Proceedings of the POPL 2006 symposium.
 <LI>Sandrine Blazy, Zaynah Dargaye and Xavier Leroy,
 <A HREF="http://gallium.inria.fr/~xleroy/publi/cfront.pdf">Formal
 verification of a C compiler front-end</A>. 
 Proceedings of Formal Methods 2006, LNCS 4085.
-<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. arXiv:0902.2137 [cs]. Draft submitted for publication, July 2008.
+<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
+Journal of Automated Reasoning 43(4):363-446, 2009.
 </UL>
 
 <P>This Web site gives a commented listing of the underlying Coq
@@ -61,7 +58,7 @@ overview papers above were written.</P>
 <A HREF="http://compcert.inria.fr/">the Compcert Web site</A>.</P>
 
 <P>This document and the Compcert sources are
-copyright 2005, 2006, 2007, 2008, 2009 Institut National de Recherche en
+copyright 2005, 2006, 2007, 2008, 2009, 2010 Institut National de Recherche en
 Informatique et en Automatique (INRIA) and distributed under the terms
 of the following <A HREF="LICENSE">license</A>.
 </P>