From 33a4bcf3695d0ee2793b3bdd12f6ee787d152f36 Mon Sep 17 00:00:00 2001
From: xleroy
Date: Tue, 12 Jan 2010 13:36:46 +0000
Subject: MAJ release 1.6
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1224 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
doc/index.html | 13 +++++--------
1 file changed, 5 insertions(+), 8 deletions(-)
(limited to 'doc')
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; }
The Compcert verified compiler
Commented Coq development
-Version 1.5, 2009-08-28
+Version 1.6, 2010-01-12
Introduction
-Compcert is a compiler that generates PowerPC assembly
+
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.
correctness can be found in the following papers (in increasing order of technical details):
- Xavier Leroy, Formal verification of a realistic compiler. Communications of the ACM 52(7), July 2009.
-
- Xavier Leroy, Formal
-certification of a compiler back-end, or: programming a compiler with
-a proof assistant. Proceedings of the POPL 2006 symposium.
- Sandrine Blazy, Zaynah Dargaye and Xavier Leroy,
Formal
verification of a C compiler front-end.
Proceedings of Formal Methods 2006, LNCS 4085.
-
- Xavier Leroy, A formally verified compiler back-end. arXiv:0902.2137 [cs]. Draft submitted for publication, July 2008.
+
- Xavier Leroy, A formally verified compiler back-end.
+Journal of Automated Reasoning 43(4):363-446, 2009.
This Web site gives a commented listing of the underlying Coq
@@ -61,7 +58,7 @@ overview papers above were written.
the Compcert Web site.
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 license.
--
cgit v1.2.3