source: Deliverables/D2.1/report.out @ 1847

Last change on this file since 1847 was 59, checked in by sacerdot, 11 years ago

Added a new appendix for assessment within the CerCo? project.
File size: 4.5 KB
Line 
1\BOOKMARK [1][]{section.1}{Introduction}{}
2\BOOKMARK [2][]{subsection.1.1}{Meaning of cost annotations}{section.1}
3\BOOKMARK [2][]{subsection.1.2}{Soundness and precision of cost annotations}{section.1}
4\BOOKMARK [2][]{subsection.1.3}{Compositionality}{section.1}
5\BOOKMARK [2][]{subsection.1.4}{Direct approach to cost annotations}{section.1}
6\BOOKMARK [2][]{subsection.1.5}{Labelling approach to cost annotations}{section.1}
7\BOOKMARK [2][]{subsection.1.6}{A toy compiler}{section.1}
8\BOOKMARK [2][]{subsection.1.7}{A C compiler}{section.1}
9\BOOKMARK [2][]{subsection.1.8}{Organisation}{section.1}
10\BOOKMARK [1][]{section.2}{A toy compiler}{}
11\BOOKMARK [2][]{subsection.2.1}{Imp: language and semantics}{section.2}
12\BOOKMARK [2][]{subsection.2.2}{Big-step semantics}{section.2}
13\BOOKMARK [2][]{subsection.2.3}{Small-step semantics}{section.2}
14\BOOKMARK [2][]{subsection.2.4}{Vm: language and semantics}{section.2}
15\BOOKMARK [2][]{subsection.2.5}{Compilation from Imp to Vm}{section.2}
16\BOOKMARK [2][]{subsection.2.6}{Soundness of compilation for the big-step semantics}{section.2}
17\BOOKMARK [2][]{subsection.2.7}{Soundness of compilation for the small-step semantics}{section.2}
18\BOOKMARK [2][]{subsection.2.8}{Compiled code is well-formed}{section.2}
19\BOOKMARK [2][]{subsection.2.9}{Mips: language and semantics}{section.2}
20\BOOKMARK [2][]{subsection.2.10}{Compilation from Vm to Mips}{section.2}
21\BOOKMARK [1][]{section.3}{Direct approach for the toy compiler}{}
22\BOOKMARK [2][]{subsection.3.1}{Mips and Vm cost annotations}{section.3}
23\BOOKMARK [2][]{subsection.3.2}{Imp cost annotation}{section.3}
24\BOOKMARK [2][]{subsection.3.3}{Composition}{section.3}
25\BOOKMARK [2][]{subsection.3.4}{Coq development}{section.3}
26\BOOKMARK [2][]{subsection.3.5}{Limitations of the direct approach}{section.3}
27\BOOKMARK [1][]{section.4}{Labelling approach for the toy compiler}{}
28\BOOKMARK [2][]{subsection.4.1}{Labelled Imp}{section.4}
29\BOOKMARK [2][]{subsection.4.2}{Labelled Vm}{section.4}
30\BOOKMARK [2][]{subsection.4.3}{Labelled Mips}{section.4}
31\BOOKMARK [2][]{subsection.4.4}{Labellings and instrumentations}{section.4}
32\BOOKMARK [2][]{subsection.4.5}{Sound and precise labellings}{section.4}
33\BOOKMARK [1][]{section.5}{A C compiler}{}
34\BOOKMARK [2][]{subsection.5.1}{Clight}{section.5}
35\BOOKMARK [2][]{subsection.5.2}{Cminor}{section.5}
36\BOOKMARK [2][]{subsection.5.3}{RTLAbs}{section.5}
37\BOOKMARK [2][]{subsection.5.4}{RTL}{section.5}
38\BOOKMARK [2][]{subsection.5.5}{ERTL}{section.5}
39\BOOKMARK [2][]{subsection.5.6}{LTL}{section.5}
40\BOOKMARK [2][]{subsection.5.7}{LIN}{section.5}
41\BOOKMARK [2][]{subsection.5.8}{Mips}{section.5}
42\BOOKMARK [1][]{section.6}{Labelling approach for the C compiler}{}
43\BOOKMARK [2][]{subsection.6.1}{Labelled Clight and labelled Cminor}{section.6}
44\BOOKMARK [2][]{subsection.6.2}{Labels in RTLAbs and the back-end languages}{section.6}
45\BOOKMARK [2][]{subsection.6.3}{Labelling of the source language}{section.6}
46\BOOKMARK [3][]{subsubsection.6.3.1}{Sequential instructions}{subsection.6.3}
47\BOOKMARK [3][]{subsubsection.6.3.2}{Ternary expressions}{subsection.6.3}
48\BOOKMARK [3][]{subsubsection.6.3.3}{Conditionals}{subsection.6.3}
49\BOOKMARK [3][]{subsubsection.6.3.4}{Loops}{subsection.6.3}
50\BOOKMARK [3][]{subsubsection.6.3.5}{Program Labels and Gotos}{subsection.6.3}
51\BOOKMARK [3][]{subsubsection.6.3.6}{Function calls}{subsection.6.3}
52\BOOKMARK [2][]{subsection.6.4}{Verifications on the object code}{section.6}
53\BOOKMARK [2][]{subsection.6.5}{Building the cost annotation}{section.6}
54\BOOKMARK [2][]{subsection.6.6}{Testing}{section.6}
55\BOOKMARK [1][]{section.7}{Conclusion and future work}{}
56\BOOKMARK [1][]{appendix.A}{Assessment of the deliverable within the CerCo project}{}
57\BOOKMARK [1][]{appendix.B}{Proofs}{}
58\BOOKMARK [2][]{subsection.B.1}{Notation}{appendix.B}
59\BOOKMARK [2][]{subsection.B.2}{Proof of proposition 4}{appendix.B}
60\BOOKMARK [2][]{subsection.B.3}{Proof of proposition 8}{appendix.B}
61\BOOKMARK [2][]{subsection.B.4}{Proof of proposition 10}{appendix.B}
62\BOOKMARK [2][]{subsection.B.5}{Proof of proposition 11}{appendix.B}
63\BOOKMARK [2][]{subsection.B.6}{Proof of proposition 13}{appendix.B}
64\BOOKMARK [2][]{subsection.B.7}{Proof of proposition 14}{appendix.B}
65\BOOKMARK [2][]{subsection.B.8}{Proof of proposition 16}{appendix.B}
66\BOOKMARK [2][]{subsection.B.9}{Proof of proposition 17}{appendix.B}
67\BOOKMARK [2][]{subsection.B.10}{Proof of proposition 20}{appendix.B}
68\BOOKMARK [2][]{subsection.B.11}{Proof of proposition 22}{appendix.B}
69\BOOKMARK [2][]{subsection.B.12}{Proof of proposition 23}{appendix.B}
70\BOOKMARK [2][]{subsection.B.13}{Proof of proposition 25}{appendix.B}
Note: See TracBrowser for help on using the repository browser.