Changeset 3355

Timestamp:

Jun 14, 2013, 3:21:21 PM (6 years ago)

Author:

sacerdot

Message:

...

File:

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

Papers/itp-2013/ccexec2.tex

@@ -166 +166 @@
 from the object code to the source code. Examples of non-functional properties
 are execution time, amount of stack/heap space consumed and energy required for
-communication. The basic idea of the approach is that it is impossible to
+communication. The basic premise of the approach is that it is impossible to
 provide a \emph{uniform} cost model for an high level language that is preserved
 \emph{precisely} by a compiler. For instance, two instances of an assignment
@@ -203 +203 @@
 architectures and caches.
 
-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
+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 optimising and implements a compilation chain that is largely
@@ -214 +214 @@
 functional properties only. In the case of a programming language with
 function calls, instead, it turns out that the forward simulation proof for
-the back-end languages must grant a whole new set of invariants.
+the back-end languages, which are unstructured, must grant a whole new set of invariants.
 
 In this paper we present a formalisation in the Matita interactive theorem