Changeset 3355


Ignore:
Timestamp:
Jun 14, 2013, 3:21:21 PM (4 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec2.tex

    r3351 r3355  
    166166from the object code to the source code. Examples of non-functional properties
    167167are execution time, amount of stack/heap space consumed and energy required for
    168 communication. The basic idea of the approach is that it is impossible to
     168communication. The basic premise of the approach is that it is impossible to
    169169provide a \emph{uniform} cost model for an high level language that is preserved
    170170\emph{precisely} by a compiler. For instance, two instances of an assignment
     
    203203architectures and caches.
    204204
    205 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
     205In 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
    2062068051 object code. The compiler is
    207207moderately optimising and implements a compilation chain that is largely
     
    214214functional properties only. In the case of a programming language with
    215215function calls, instead, it turns out that the forward simulation proof for
    216 the back-end languages must grant a whole new set of invariants.
     216the back-end languages, which are unstructured, must grant a whole new set of invariants.
    217217
    218218In this paper we present a formalisation in the Matita interactive theorem
Note: See TracChangeset for help on using the changeset viewer.