Changeset 1982 for Deliverables/D2.1/report.out
 Timestamp:
 May 22, 2012, 8:14:57 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.1/report.out
r59 r1982 1 1 \BOOKMARK [1][]{section.1}{Introduction}{} 2 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}{Bigstep semantics}{section.2}13 \BOOKMARK [2][]{subsection.2.3}{Smallstep 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 bigstep semantics}{section.2}17 \BOOKMARK [2][]{subsection.2.7}{Soundness of compilation for the smallstep semantics}{section.2}18 \BOOKMARK [2][]{subsection.2.8}{Compiled code is wellformed}{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 backend 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 TracChangeset
for help on using the changeset viewer.