| 1 | \relax |
|---|
| 2 | \ifx\hyper@anchor\@undefined |
|---|
| 3 | \global \let \oldcontentsline\contentsline |
|---|
| 4 | \gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}} |
|---|
| 5 | \global \let \oldnewlabel\newlabel |
|---|
| 6 | \gdef \newlabel#1#2{\newlabelxx{#1}#2} |
|---|
| 7 | \gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}} |
|---|
| 8 | \AtEndDocument{\let \contentsline\oldcontentsline |
|---|
| 9 | \let \newlabel\oldnewlabel} |
|---|
| 10 | \else |
|---|
| 11 | \global \let \hyper@last\relax |
|---|
| 12 | \fi |
|---|
| 13 | |
|---|
| 14 | \bibstyle{abbrv} |
|---|
| 15 | \select@language{english} |
|---|
| 16 | \@writefile{toc}{\select@language{english}} |
|---|
| 17 | \@writefile{lof}{\select@language{english}} |
|---|
| 18 | \@writefile{lot}{\select@language{english}} |
|---|
| 19 | \@writefile{toc}{\contentsline {paragraph}{Abstract}{2}{section*.1}} |
|---|
| 20 | \citation{Leroy09} |
|---|
| 21 | \citation{Cerco10} |
|---|
| 22 | \citation{SCADE} |
|---|
| 23 | \citation{Fornari10} |
|---|
| 24 | \citation{AbsInt} |
|---|
| 25 | \citation{AbsintScade} |
|---|
| 26 | \citation{W09} |
|---|
| 27 | \citation{Frama-C} |
|---|
| 28 | \@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{5}{section.1}} |
|---|
| 29 | \newlabel{intro-sec}{{1}{5}{Introduction\relax }{section.1}{}} |
|---|
| 30 | \@writefile{toc}{\contentsline {paragraph}{Meaning of cost annotations}{5}{section*.3}} |
|---|
| 31 | \@writefile{toc}{\contentsline {paragraph}{Soundness and precision of cost annotations}{6}{section*.4}} |
|---|
| 32 | \newlabel{comp-intro}{{1}{6}{Compositionality\relax }{section*.5}{}} |
|---|
| 33 | \@writefile{toc}{\contentsline {paragraph}{Compositionality}{6}{section*.5}} |
|---|
| 34 | \newlabel{label-intro}{{1}{6}{Labelling approach to cost annotations\relax }{section*.6}{}} |
|---|
| 35 | \@writefile{toc}{\contentsline {paragraph}{Labelling approach to cost annotations}{6}{section*.6}} |
|---|
| 36 | \newlabel{STEP1}{{1}{7}{Labelling approach to cost annotations\relax }{equation.1.1}{}} |
|---|
| 37 | \newlabel{step2}{{2}{7}{Labelling approach to cost annotations\relax }{equation.1.2}{}} |
|---|
| 38 | \newlabel{toy-intro}{{1}{7}{A toy compiler\relax }{section*.7}{}} |
|---|
| 39 | \@writefile{toc}{\contentsline {paragraph}{A toy compiler}{7}{section*.7}} |
|---|
| 40 | \citation{Leroy09} |
|---|
| 41 | \citation{CIL02} |
|---|
| 42 | \citation{Pottier} |
|---|
| 43 | \citation{intel94} |
|---|
| 44 | \citation{share} |
|---|
| 45 | \newlabel{Ccompiler-intro}{{1}{8}{A C compiler\relax }{section*.8}{}} |
|---|
| 46 | \@writefile{toc}{\contentsline {paragraph}{A C compiler}{8}{section*.8}} |
|---|
| 47 | \@writefile{toc}{\contentsline {paragraph}{Organization}{8}{section*.9}} |
|---|
| 48 | \@writefile{toc}{\contentsline {section}{\numberline {2}Labelling approach for the toy compiler}{8}{section.2}} |
|---|
| 49 | \newlabel{label-toy-sec}{{2}{8}{Labelling approach for the toy compiler\relax }{section.2}{}} |
|---|
| 50 | \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Syntax definitions.}}{9}{figure.1}} |
|---|
| 51 | \newlabel{fig:syntaxes}{{1}{9}{Syntax definitions}{figure.1}{}} |
|---|
| 52 | \@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Labelled ${\sf Imp}$}{9}{subsection.2.1}} |
|---|
| 53 | \@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Labelled ${\sf Vm}$}{9}{subsection.2.2}} |
|---|
| 54 | \newlabel{labelled-sim-imp-vm}{{1}{10}{Labelled $\vm $\relax }{theorem.1}{}} |
|---|
| 55 | \newlabel{rem:multi-set}{{2}{10}{Labelled $\vm $\relax }{theorem.2}{}} |
|---|
| 56 | \@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Labelled ${\sf Mips}$}{10}{subsection.2.3}} |
|---|
| 57 | \newlabel{sim-vm-mips-prop}{{3}{10}{Labelled $\mips $\relax }{theorem.3}{}} |
|---|
| 58 | \@writefile{toc}{\contentsline {subsection}{\numberline {2.4}Labellings and instrumentations}{10}{subsection.2.4}} |
|---|
| 59 | \newlabel{lab-instr-erasure-imp}{{4}{11}{Labellings and instrumentations\relax }{theorem.4}{}} |
|---|
| 60 | \newlabel{labelling-def}{{5}{11}{Labellings and instrumentations\relax }{theorem.5}{}} |
|---|
| 61 | \newlabel{global-commutation-prop}{{6}{11}{Labellings and instrumentations\relax }{theorem.6}{}} |
|---|
| 62 | \newlabel{instrument-to-label-prop}{{7}{11}{Labellings and instrumentations\relax }{theorem.7}{}} |
|---|
| 63 | \@writefile{toc}{\contentsline {subsection}{\numberline {2.5}Sound and precise labellings}{11}{subsection.2.5}} |
|---|
| 64 | \newlabel{sound-label-sec}{{2.5}{11}{Sound and precise labellings\relax }{subsection.2.5}{}} |
|---|
| 65 | \newlabel{sound-label-prop}{{10}{11}{Sound and precise labellings\relax }{theorem.10}{}} |
|---|
| 66 | \newlabel{precise-label-prop}{{12}{11}{Sound and precise labellings\relax }{theorem.12}{}} |
|---|
| 67 | \@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Two labellings for the ${\sf Imp}$ language}}{12}{table.1}} |
|---|
| 68 | \newlabel{labelling}{{1}{12}{Two labellings for the $\imp $ language\relax }{table.1}{}} |
|---|
| 69 | \newlabel{lab-sound}{{13}{12}{Sound and precise labellings\relax }{theorem.13}{}} |
|---|
| 70 | \newlabel{ann-correct}{{15}{12}{Sound and precise labellings\relax }{theorem.15}{}} |
|---|
| 71 | \@writefile{toc}{\contentsline {section}{\numberline {3}Labelling approach for the ${\sf C}$ compiler}{13}{section.3}} |
|---|
| 72 | \newlabel{C-label-sec}{{3}{13}{Labelling approach for the $\C $ compiler\relax }{section.3}{}} |
|---|
| 73 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Labelled languages}{13}{subsection.3.1}} |
|---|
| 74 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Labelling of the source language}{14}{subsection.3.2}} |
|---|
| 75 | \@writefile{toc}{\contentsline {paragraph}{Sequential instructions}{14}{section*.10}} |
|---|
| 76 | \@writefile{toc}{\contentsline {paragraph}{Ternary expressions and conditionals}{14}{section*.11}} |
|---|
| 77 | \@writefile{toc}{\contentsline {paragraph}{Loops}{14}{section*.12}} |
|---|
| 78 | \@writefile{toc}{\contentsline {paragraph}{Program Labels and Gotos}{14}{section*.13}} |
|---|
| 79 | \newlabel{fun-call-sec}{{3.2}{14}{Function calls\relax }{section*.14}{}} |
|---|
| 80 | \@writefile{toc}{\contentsline {paragraph}{Function calls}{14}{section*.14}} |
|---|
| 81 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Verifications on the object code}{15}{subsection.3.3}} |
|---|
| 82 | \citation{Cerco10} |
|---|
| 83 | \bibcite{AbsInt}{1} |
|---|
| 84 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Building the cost annotation}{16}{subsection.3.4}} |
|---|
| 85 | \@writefile{toc}{\contentsline {subsection}{\numberline {3.5}Testing}{16}{subsection.3.5}} |
|---|
| 86 | \@writefile{toc}{\contentsline {section}{\numberline {4}Conclusion and future work}{16}{section.4}} |
|---|
| 87 | \newlabel{conclusion-sec}{{4}{16}{Conclusion and future work\relax }{section.4}{}} |
|---|
| 88 | \bibcite{Cerco10}{2} |
|---|
| 89 | \bibcite{SCADE}{3} |
|---|
| 90 | \bibcite{Frama-C}{4} |
|---|
| 91 | \bibcite{AbsintScade}{5} |
|---|
| 92 | \bibcite{Fornari10}{6} |
|---|
| 93 | \bibcite{Larus05}{7} |
|---|
| 94 | \bibcite{intel94}{8} |
|---|
| 95 | \bibcite{Leroy09}{9} |
|---|
| 96 | \bibcite{Leroy09-ln}{10} |
|---|
| 97 | \bibcite{CIL02}{11} |
|---|
| 98 | \bibcite{Pottier}{12} |
|---|
| 99 | \bibcite{W09}{13} |
|---|
| 100 | \bibcite{share}{14} |
|---|
| 101 | \citation{Leroy09-ln} |
|---|
| 102 | \@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Small-step operational semantics of ${\sf Imp}$ commands}}{18}{table.2}} |
|---|
| 103 | \newlabel{small-step-imp}{{2}{18}{Small-step operational semantics of $\imp $ commands\relax }{table.2}{}} |
|---|
| 104 | \@writefile{toc}{\contentsline {section}{\numberline {A}A toy compiler}{18}{appendix.A}} |
|---|
| 105 | \newlabel{toy-compiler-sec}{{A}{18}{A toy compiler\relax }{appendix.A}{}} |
|---|
| 106 | \@writefile{toc}{\contentsline {subsection}{\numberline {A.1}{\sf Imp}: language and semantics}{18}{subsection.A.1}} |
|---|
| 107 | \newlabel{imp-sec}{{A.1}{18}{\imp : language and semantics\relax }{subsection.A.1}{}} |
|---|
| 108 | \@writefile{toc}{\contentsline {subsection}{\numberline {A.2}{\sf Vm}: language and semantics}{18}{subsection.A.2}} |
|---|
| 109 | \newlabel{vm-sec}{{A.2}{18}{\vm : language and semantics\relax }{subsection.A.2}{}} |
|---|
| 110 | \citation{Leroy09-ln} |
|---|
| 111 | \@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces Operational semantics ${\sf Vm}$ programs}}{19}{table.3}} |
|---|
| 112 | \newlabel{semantics-vm}{{3}{19}{Operational semantics $\vm $ programs\relax }{table.3}{}} |
|---|
| 113 | \@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Conditions for well-formed code}}{19}{table.4}} |
|---|
| 114 | \newlabel{well-formed-instr}{{4}{19}{Conditions for well-formed code\relax }{table.4}{}} |
|---|
| 115 | \newlabel{unicity-height-prop}{{17}{19}{\vm : language and semantics\relax }{theorem.17}{}} |
|---|
| 116 | \@writefile{toc}{\contentsline {subsection}{\numberline {A.3}Compilation from ${\sf Imp}$ to ${\sf Vm}$}{19}{subsection.A.3}} |
|---|
| 117 | \newlabel{compil-imp-vm-sec}{{A.3}{19}{Compilation from $\imp $ to $\vm $\relax }{subsection.A.3}{}} |
|---|
| 118 | \citation{Larus05} |
|---|
| 119 | \@writefile{lot}{\contentsline {table}{\numberline {5}{\ignorespaces Compilation from ${\sf Imp}$ to ${\sf Vm}$}}{20}{table.5}} |
|---|
| 120 | \newlabel{compil-imp-vm}{{5}{20}{Compilation from $\imp $ to $\vm $\relax }{table.5}{}} |
|---|
| 121 | \newlabel{soundness-big-step-prop}{{18}{20}{Compilation from $\imp $ to $\vm $\relax }{theorem.18}{}} |
|---|
| 122 | \newlabel{soundness-small-step}{{19}{20}{Compilation from $\imp $ to $\vm $\relax }{theorem.19}{}} |
|---|
| 123 | \newlabel{well-formed-prop}{{20}{20}{Compilation from $\imp $ to $\vm $\relax }{theorem.20}{}} |
|---|
| 124 | \@writefile{toc}{\contentsline {subsection}{\numberline {A.4}${\sf Mips}$: language and semantics}{20}{subsection.A.4}} |
|---|
| 125 | \newlabel{mips-sec}{{A.4}{20}{$\mips $: language and semantics\relax }{subsection.A.4}{}} |
|---|
| 126 | \@writefile{lot}{\contentsline {table}{\numberline {6}{\ignorespaces Operational semantics ${\sf Mips}$ programs}}{21}{table.6}} |
|---|
| 127 | \newlabel{semantics-mips}{{6}{21}{Operational semantics $\mips $ programs\relax }{table.6}{}} |
|---|
| 128 | \@writefile{lot}{\contentsline {table}{\numberline {7}{\ignorespaces Compilation from ${\sf Vm}$ to ${\sf Mips}$}}{21}{table.7}} |
|---|
| 129 | \newlabel{compil-vm-mips}{{7}{21}{Compilation from $\vm $ to $\mips $\relax }{table.7}{}} |
|---|
| 130 | \@writefile{toc}{\contentsline {subsection}{\numberline {A.5}Compilation from ${\sf Vm}$ to ${\sf Mips}$}{21}{subsection.A.5}} |
|---|
| 131 | \newlabel{compil-vm-mips-sec}{{A.5}{21}{Compilation from $\vm $ to $\mips $\relax }{subsection.A.5}{}} |
|---|
| 132 | \newlabel{simulation-vm-mips}{{21}{22}{Compilation from $\vm $ to $\mips $\relax }{theorem.21}{}} |
|---|
| 133 | \@writefile{toc}{\contentsline {section}{\numberline {B}Proofs}{23}{appendix.B}} |
|---|
| 134 | \newlabel{paper-proofs}{{B}{23}{Proofs\relax }{appendix.B}{}} |
|---|
| 135 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.1}Notation}{23}{subsection.B.1}} |
|---|
| 136 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {labelled-sim-imp-vm}}{23}{subsection.B.2}} |
|---|
| 137 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {sim-vm-mips-prop}}{23}{subsection.B.3}} |
|---|
| 138 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {lab-instr-erasure-imp}}{23}{subsection.B.4}} |
|---|
| 139 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {global-commutation-prop}}{24}{subsection.B.5}} |
|---|
| 140 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {instrument-to-label-prop}}{24}{subsection.B.6}} |
|---|
| 141 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {sound-label-prop}}{24}{subsection.B.7}} |
|---|
| 142 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {precise-label-prop}}{24}{subsection.B.8}} |
|---|
| 143 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {lab-sound}}{25}{subsection.B.9}} |
|---|
| 144 | \newlabel{precise-lemma}{{24}{25}{Proof of proposition \ref {lab-sound}\relax }{theorem.24}{}} |
|---|
| 145 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {ann-correct}}{25}{subsection.B.10}} |
|---|
| 146 | \@writefile{toc}{\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {soundness-small-step}}{25}{subsection.B.11}} |
|---|
| 147 | \newlabel{access-lemma}{{25}{25}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.25}{}} |
|---|
| 148 | \citation{CIL02} |
|---|
| 149 | \citation{Leroy09} |
|---|
| 150 | \@writefile{toc}{\contentsline {section}{\numberline {C}A ${\sf C}$ compiler}{27}{appendix.C}} |
|---|
| 151 | \newlabel{C-compiler-sec}{{C}{27}{A $\C $ compiler\relax }{appendix.C}{}} |
|---|
| 152 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.1}${\sf Clight}$}{27}{subsection.C.1}} |
|---|
| 153 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.2}${\sf Cminor}$}{27}{subsection.C.2}} |
|---|
| 154 | \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf Clight}$ to ${\sf Cminor}$}{27}{section*.16}} |
|---|
| 155 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.3}${\sf RTLAbs}$}{27}{subsection.C.3}} |
|---|
| 156 | \newlabel{syntax-clight}{{C.1}{28}{$\Clight $\relax }{subsection.C.1}{}} |
|---|
| 157 | \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Syntax of the ${\sf Clight}$ language}}{28}{figure.2}} |
|---|
| 158 | \newlabel{syntax-cminor}{{C.2}{29}{$\Cminor $\relax }{subsection.C.2}{}} |
|---|
| 159 | \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Syntax of the ${\sf Cminor}$ language}}{29}{figure.3}} |
|---|
| 160 | \@writefile{lot}{\contentsline {table}{\numberline {8}{\ignorespaces Syntax of the ${\sf RTLAbs}$ language}}{30}{table.8}} |
|---|
| 161 | \newlabel{RTLAbs:syntax}{{8}{30}{Syntax of the $\RTLAbs $ language\relax }{table.8}{}} |
|---|
| 162 | \@writefile{toc}{\contentsline {paragraph}{Syntax.}{30}{section*.17}} |
|---|
| 163 | \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf Cminor}$ to ${\sf RTLAbs}$.}{30}{section*.18}} |
|---|
| 164 | \@writefile{lot}{\contentsline {table}{\numberline {9}{\ignorespaces Syntax of the ${\sf RTL}$ language}}{31}{table.9}} |
|---|
| 165 | \newlabel{RTL:syntax}{{9}{31}{Syntax of the $\RTL $ language\relax }{table.9}{}} |
|---|
| 166 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.4}${\sf RTL}$}{31}{subsection.C.4}} |
|---|
| 167 | \@writefile{toc}{\contentsline {paragraph}{Syntax.}{31}{section*.19}} |
|---|
| 168 | \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf RTLAbs}$ to ${\sf RTL}$.}{31}{section*.20}} |
|---|
| 169 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.5}${\sf ERTL}$}{31}{subsection.C.5}} |
|---|
| 170 | \@writefile{lot}{\contentsline {table}{\numberline {10}{\ignorespaces Syntax of the ${\sf ERTL}$ language}}{32}{table.10}} |
|---|
| 171 | \newlabel{ERTL:syntax}{{10}{32}{Syntax of the $\ERTL $ language\relax }{table.10}{}} |
|---|
| 172 | \@writefile{toc}{\contentsline {paragraph}{Syntax.}{32}{section*.21}} |
|---|
| 173 | \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf RTL}$ to ${\sf ERTL}$.}{32}{section*.22}} |
|---|
| 174 | \@writefile{lot}{\contentsline {table}{\numberline {11}{\ignorespaces Syntax of the ${\sf LTL}$ language}}{33}{table.11}} |
|---|
| 175 | \newlabel{LTL:syntax}{{11}{33}{Syntax of the $\LTL $ language\relax }{table.11}{}} |
|---|
| 176 | \@writefile{toc}{\contentsline {paragraph}{Optimizations.}{33}{section*.23}} |
|---|
| 177 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.6}${\sf LTL}$}{33}{subsection.C.6}} |
|---|
| 178 | \@writefile{toc}{\contentsline {paragraph}{Syntax.}{33}{section*.24}} |
|---|
| 179 | \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf ERTL}$ to ${\sf LTL}$.}{33}{section*.25}} |
|---|
| 180 | \@writefile{toc}{\contentsline {paragraph}{Optimizations.}{33}{section*.26}} |
|---|
| 181 | \citation{intel94} |
|---|
| 182 | \@writefile{lot}{\contentsline {table}{\numberline {12}{\ignorespaces Syntax of the ${\sf LIN}$ language}}{34}{table.12}} |
|---|
| 183 | \newlabel{LIN:syntax}{{12}{34}{Syntax of the $\LIN $ language\relax }{table.12}{}} |
|---|
| 184 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.7}${\sf LIN}$}{34}{subsection.C.7}} |
|---|
| 185 | \@writefile{toc}{\contentsline {paragraph}{Syntax.}{34}{section*.27}} |
|---|
| 186 | \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf LTL}$ to ${\sf LIN}$.}{34}{section*.28}} |
|---|
| 187 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.8}Assembly}{34}{subsection.C.8}} |
|---|
| 188 | \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf LIN}$ to ${\sf Mips}$.}{34}{section*.29}} |
|---|
| 189 | \@writefile{lot}{\contentsline {table}{\numberline {13}{\ignorespaces Syntax of the ${\sf Mips}$ language}}{35}{table.13}} |
|---|
| 190 | \newlabel{mips:syntax}{{13}{35}{Syntax of the $\mips $ language\relax }{table.13}{}} |
|---|
| 191 | \@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Benchmarks results (execution time is given in seconds).}}{35}{figure.4}} |
|---|
| 192 | \newlabel{fig:benchmark-results}{{4}{35}{Benchmarks results (execution time is given in seconds)}{figure.4}{}} |
|---|
| 193 | \@writefile{toc}{\contentsline {subsection}{\numberline {C.9}Benchmarks}{36}{subsection.C.9}} |
|---|
| 194 | \newlabel{C-compiler-benchmarks}{{C.9}{36}{Benchmarks\relax }{subsection.C.9}{}} |
|---|
| 195 | \@writefile{toc}{\contentsline {section}{\numberline {D}A direct approach}{37}{appendix.D}} |
|---|
| 196 | \newlabel{direct-sec}{{D}{37}{A direct approach\relax }{appendix.D}{}} |
|---|
| 197 | \@writefile{toc}{\contentsline {subsection}{\numberline {D.1}${\sf Mips}$ and ${\sf Vm}$ cost annotations}{37}{subsection.D.1}} |
|---|
| 198 | \@writefile{lot}{\contentsline {table}{\numberline {14}{\ignorespaces Upper bounds on the cost of ${\sf Vm}$ instructions}}{38}{table.14}} |
|---|
| 199 | \newlabel{cost-approx-instr}{{14}{38}{Upper bounds on the cost of $\vm $ instructions\relax }{table.14}{}} |
|---|
| 200 | \newlabel{annot-vm-mips}{{26}{38}{$\mips $ and $\vm $ cost annotations\relax }{theorem.26}{}} |
|---|
| 201 | \newlabel{labelled-simulation-vm-mips}{{27}{38}{$\mips $ and $\vm $ cost annotations\relax }{theorem.27}{}} |
|---|
| 202 | \@writefile{toc}{\contentsline {subsection}{\numberline {D.2}${\sf Imp}$ cost annotation}{38}{subsection.D.2}} |
|---|
| 203 | \newlabel{imp-cost-annotation}{{D.2}{38}{$\imp $ cost annotation\relax }{subsection.D.2}{}} |
|---|
| 204 | \@writefile{lot}{\contentsline {table}{\numberline {15}{\ignorespaces Annotation for ${\sf Imp}$ programs}}{39}{table.15}} |
|---|
| 205 | \newlabel{annotation-imp}{{15}{39}{Annotation for $\imp $ programs\relax }{table.15}{}} |
|---|
| 206 | \newlabel{annot-imp-vm}{{28}{39}{$\imp $ cost annotation\relax }{theorem.28}{}} |
|---|
| 207 | \citation{Leroy09-ln} |
|---|
| 208 | \@writefile{toc}{\contentsline {subsection}{\numberline {D.3}Composition}{40}{subsection.D.3}} |
|---|
| 209 | \newlabel{annot-composition}{{29}{40}{Composition\relax }{theorem.29}{}} |
|---|
| 210 | \@writefile{toc}{\contentsline {subsection}{\numberline {D.4}${\sf Coq}$ development}{40}{subsection.D.4}} |
|---|
| 211 | \newlabel{coq-development-sec}{{D.4}{40}{$\coq $ development\relax }{subsection.D.4}{}} |
|---|
| 212 | \@writefile{toc}{\contentsline {subsection}{\numberline {D.5}Limitations of the direct approach}{40}{subsection.D.5}} |
|---|
| 213 | \newlabel{limitations-direct-sec}{{D.5}{40}{Limitations of the direct approach\relax }{subsection.D.5}{}} |
|---|
| 214 | \@writefile{toc}{\contentsline {section}{\numberline {E}Related approaches}{41}{appendix.E}} |
|---|
| 215 | \newlabel{related-sec}{{E}{41}{Related approaches\relax }{appendix.E}{}} |
|---|
| 216 | \@writefile{toc}{\contentsline {section}{\numberline {F}Assessment of the deliverable within the $CerCo$ project, with hindsight}{42}{appendix.F}} |
|---|
| 217 | \newlabel{asmt-sec}{{F}{42}{Assessment of the deliverable within the $\cerco $ project, with hindsight\relax }{appendix.F}{}} |
|---|
