diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/index.html | 23 |
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> |