source: Deliverables/D2.1/Revision/report.out @ 792

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

Deliverable D2.1 with addendum

File size: 3.1 KB
Line 
1\BOOKMARK [1][]{section.1}{Introduction}{}
2\BOOKMARK [1][]{section.2}{Labelling approach for the toy compiler}{}
3\BOOKMARK [2][]{subsection.2.1}{Labelled Imp}{section.2}
4\BOOKMARK [2][]{subsection.2.2}{Labelled Vm}{section.2}
5\BOOKMARK [2][]{subsection.2.3}{Labelled Mips}{section.2}
6\BOOKMARK [2][]{subsection.2.4}{Labellings and instrumentations}{section.2}
7\BOOKMARK [2][]{subsection.2.5}{Sound and precise labellings}{section.2}
8\BOOKMARK [1][]{section.3}{Labelling approach for the C compiler}{}
9\BOOKMARK [2][]{subsection.3.1}{Labelled languages}{section.3}
10\BOOKMARK [2][]{subsection.3.2}{Labelling of the source language}{section.3}
11\BOOKMARK [2][]{subsection.3.3}{Verifications on the object code}{section.3}
12\BOOKMARK [2][]{subsection.3.4}{Building the cost annotation}{section.3}
13\BOOKMARK [2][]{subsection.3.5}{Testing}{section.3}
14\BOOKMARK [1][]{section.4}{Conclusion and future work}{}
15\BOOKMARK [1][]{appendix.A}{A toy compiler}{}
16\BOOKMARK [2][]{subsection.A.1}{Imp: language and semantics}{appendix.A}
17\BOOKMARK [2][]{subsection.A.2}{Vm: language and semantics}{appendix.A}
18\BOOKMARK [2][]{subsection.A.3}{Compilation from Imp to Vm}{appendix.A}
19\BOOKMARK [2][]{subsection.A.4}{Mips: language and semantics}{appendix.A}
20\BOOKMARK [2][]{subsection.A.5}{Compilation from Vm to Mips}{appendix.A}
21\BOOKMARK [1][]{appendix.B}{Proofs}{}
22\BOOKMARK [2][]{subsection.B.1}{Notation}{appendix.B}
23\BOOKMARK [2][]{subsection.B.2}{Proof of proposition 1}{appendix.B}
24\BOOKMARK [2][]{subsection.B.3}{Proof of proposition 3}{appendix.B}
25\BOOKMARK [2][]{subsection.B.4}{Proof of proposition 4}{appendix.B}
26\BOOKMARK [2][]{subsection.B.5}{Proof of proposition 6}{appendix.B}
27\BOOKMARK [2][]{subsection.B.6}{Proof of proposition 7}{appendix.B}
28\BOOKMARK [2][]{subsection.B.7}{Proof of proposition 10}{appendix.B}
29\BOOKMARK [2][]{subsection.B.8}{Proof of proposition 12}{appendix.B}
30\BOOKMARK [2][]{subsection.B.9}{Proof of proposition 13}{appendix.B}
31\BOOKMARK [2][]{subsection.B.10}{Proof of proposition 15}{appendix.B}
32\BOOKMARK [2][]{subsection.B.11}{Proof of proposition 19}{appendix.B}
33\BOOKMARK [1][]{appendix.C}{A C compiler}{}
34\BOOKMARK [2][]{subsection.C.1}{Clight}{appendix.C}
35\BOOKMARK [2][]{subsection.C.2}{Cminor}{appendix.C}
36\BOOKMARK [2][]{subsection.C.3}{RTLAbs}{appendix.C}
37\BOOKMARK [2][]{subsection.C.4}{RTL}{appendix.C}
38\BOOKMARK [2][]{subsection.C.5}{ERTL}{appendix.C}
39\BOOKMARK [2][]{subsection.C.6}{LTL}{appendix.C}
40\BOOKMARK [2][]{subsection.C.7}{LIN}{appendix.C}
41\BOOKMARK [2][]{subsection.C.8}{Assembly}{appendix.C}
42\BOOKMARK [2][]{subsection.C.9}{Benchmarks}{appendix.C}
43\BOOKMARK [1][]{appendix.D}{A direct approach}{}
44\BOOKMARK [2][]{subsection.D.1}{Mips and Vm cost annotations}{appendix.D}
45\BOOKMARK [2][]{subsection.D.2}{Imp cost annotation}{appendix.D}
46\BOOKMARK [2][]{subsection.D.3}{Composition}{appendix.D}
47\BOOKMARK [2][]{subsection.D.4}{Coq development}{appendix.D}
48\BOOKMARK [2][]{subsection.D.5}{Limitations of the direct approach}{appendix.D}
49\BOOKMARK [1][]{appendix.E}{Related approaches}{}
50\BOOKMARK [1][]{appendix.F}{Assessment of the deliverable within the CerCo project, with hindsight}{}
Note: See TracBrowser for help on using the repository browser.