summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/index.html23
1 files changed, 12 insertions, 11 deletions
diff --git a/doc/index.html b/doc/index.html
index a5741f5..47c849e 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ 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.3, 2008-08-11</H3>
+<H3 align="center">Version 1.4, 2009-04-21</H3>
<H2>Introduction</H2>
@@ -36,10 +36,10 @@ correctness --- the fact that the generated assembly code is
semantically equivalent to its source program --- was entirely proved
within the Coq proof assistant.</P>
-<P>A high-level overview of the Compcert compiler and its proof of
-correctness can be found in the following papers:</P>
+<P>High-level descriptions of the Compcert compiler and its proof of
+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-backend.pdf">A formally verified compiler back-end</A>. Draft submitted for publication, July 2008.
+<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
@@ -48,6 +48,7 @@ a proof assistant</A>. Proceedings of the POPL 2006 symposium.
<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.
</UL>
<P>This Web site gives a commented listing of the underlying Coq
@@ -127,7 +128,7 @@ spilling, reloading and enforcement of calling conventions.
view of the activation record. <BR>
See also: <A HREF="html/Machabstr.html">Machabstr</A> abstract semantics for Mach. <BR>
See also: <A HREF="html/Machconcr.html">Machconcr</A> concrete semantics for Mach.
-<LI> <A HREF="html/PPC.html">PPC</A>: abstract syntax for PowerPC assembly
+<LI> <A HREF="html/Asm.html">Asm</A>: abstract syntax for PowerPC assembly
code.
</UL>
@@ -238,15 +239,15 @@ code.
<TD>Storing the activation records in memory</TD>
<TD>Mach to Mach</TD>
<TD>(none)
- <TD><A HREF="html/PPCgenretaddr.html">PPCgenretaddr</A><BR>
+ <TD><A HREF="html/Asmgenretaddr.html">Asmgenretaddr</A><BR>
<A HREF="html/Machabstr2concr.html">Machabstr2concr</A></TD>
<TR valign="top">
- <TD>Emission of PowerPC assembly</TD>
- <TD>Mach to PPC</TD>
- <TD><A HREF="html/PPCgen.html">PPCgen</A></TD>
- <TD><A HREF="html/PPCgenproof1.html">PPCgenproof1</A><BR>
- <A HREF="html/PPCgenproof.html">PPCgenproof</A></TD>
+ <TD>Emission of assembly code</TD>
+ <TD>Mach to Asm</TD>
+ <TD><A HREF="html/Asmgen.html">Asmgen</A></TD>
+ <TD><A HREF="html/Asmgenproof1.html">Asmgenproof1</A><BR>
+ <A HREF="html/Asmgenproof.html">Asmgenproof</A></TD>
</TR>
</TABLE>