Changeset 2609 for Papers/itp-2013/ccexec.tex

Timestamp:

Feb 6, 2013, 1:56:01 PM (9 years ago)

Author:

sacerdot

Message:

Bibliography in place.

File:

• Papers/itp-2013/ccexec.tex (modified) (3 diffs)

Papers/itp-2013/ccexec.tex

@@ -93 +93 @@
 architectures and caches.
 
-In the European Project CerCo (Certified Complexity~\footnote{\url{http://cerco.cs.unibo.it}}) we are certifying a labelling approach based compiler for a large subset of C to
+In the European Project CerCo (Certified Complexity~\footnote{\url{http://cerco.cs.unibo.it}})~\cite{cerco} we are certifying a labelling approach based compiler for a large subset of C to
 8051 object code. The compiler is
 moderately optimizing and implements a compilation chain that is largely
-inspired to that of CompCert~\cite{compcert}. Compared to work done in~\cite{easylabelling}, the main novely and source of difficulties is due to the presence
+inspired to that of CompCert~\cite{compcert1,compcert2}. Compared to work done in~\cite{easylabelling}, the main novely and source of difficulties is due to the presence
 of function calls. Surprisingly, the addition of function calls require a
 rivisitation of the proof technique given in~\cite{easylabelling}. In
@@ -172 +172 @@
 This correctness property is called in the litterature a forward simulation
 and is sufficient for correctness when the target language is
-deterministic~\cite{leroy}.
+deterministic~\cite{compcert3}.
 We also require a stronger, non-functional preservation property: after each
 pass all basic blocks must start with an emission statement, and all labels
@@ -890 +890 @@
 precise cost model on the source code in order to establish non-functional
 properties of programs on an high level language. Traditional certifications
-of compilers, like~\cite{compcert,python}, only explicitly prove preservation
+of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
 of the functional properties via forward simulations.