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}{} |
---|