Changeset 3355
- Timestamp:
- Jun 14, 2013, 3:21:21 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/itp-2013/ccexec2.tex
r3351 r3355 166 166 from the object code to the source code. Examples of non-functional properties 167 167 are execution time, amount of stack/heap space consumed and energy required for 168 communication. The basic ideaof the approach is that it is impossible to168 communication. The basic premise of the approach is that it is impossible to 169 169 provide a \emph{uniform} cost model for an high level language that is preserved 170 170 \emph{precisely} by a compiler. For instance, two instances of an assignment … … 203 203 architectures and caches. 204 204 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 to205 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 206 206 8051 object code. The compiler is 207 207 moderately optimising and implements a compilation chain that is largely … … 214 214 functional properties only. In the case of a programming language with 215 215 function calls, instead, it turns out that the forward simulation proof for 216 the back-end languages must grant a whole new set of invariants.216 the back-end languages, which are unstructured, must grant a whole new set of invariants. 217 217 218 218 In this paper we present a formalisation in the Matita interactive theorem
Note: See TracChangeset
for help on using the changeset viewer.