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):

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