source: Deliverables/D2.1/Revision/abstract.tex @ 1635

Last change on this file since 1635 was 792, checked in by amadio, 10 years ago

Deliverable D2.1 with addendum

File size: 872 bytes
1We discuss the problem of building a compiler which can {\em lift} in
2a provably correct way pieces of information on the execution cost of
3the object code to cost annotations on the source code.  To this end,
4we need a clear and flexible picture of: (i) the meaning of cost
5annotations, (ii) the method to prove them sound and precise, and
6(iii) the way such proofs can be composed.  We propose a so-called
7{\em labelling} approach to these three questions.  As a first step,
8we examine its application to a toy compiler. This formal study
9suggests that the labelling approach has good compositionality and
10scalability properties.  In order to provide further evidence for this
11claim, we report our successful experience in implementing and testing
12the labelling approach on top of a prototype compiler written in
13$\ocaml$ for (a large fragment of) the {\sc C} language.
Note: See TracBrowser for help on using the repository browser.