Ignore:
Timestamp:
May 22, 2012, 8:14:57 AM (8 years ago)
Author:
amadio
Message:

add 2.1 Survey

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.1/report.aux

    r59 r1982  
    2626\citation{W09}
    2727\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 {subsection}{\numberline {1.1}Meaning of cost annotations}{5}{subsection.1.1}}
    31 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Soundness and precision of cost annotations}{6}{subsection.1.2}}
    32 \@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Compositionality}{6}{subsection.1.3}}
    33 \newlabel{comp-intro}{{1.3}{6}{Compositionality\relax }{subsection.1.3}{}}
    34 \@writefile{toc}{\contentsline {subsection}{\numberline {1.4}Direct approach to cost annotations}{6}{subsection.1.4}}
    35 \newlabel{direct-intro}{{1.4}{6}{Direct approach to cost annotations\relax }{subsection.1.4}{}}
    36 \@writefile{toc}{\contentsline {subsection}{\numberline {1.5}Labelling approach to cost annotations}{7}{subsection.1.5}}
    37 \newlabel{label-intro}{{1.5}{7}{Labelling approach to cost annotations\relax }{subsection.1.5}{}}
    38 \newlabel{STEP1}{{1}{7}{Labelling approach to cost annotations\relax }{equation.1.1}{}}
    39 \citation{CIL02}
    40 \citation{Pottier}
    41 \newlabel{step2}{{2}{8}{Labelling approach to cost annotations\relax }{equation.1.2}{}}
    42 \@writefile{toc}{\contentsline {subsection}{\numberline {1.6}A toy compiler}{8}{subsection.1.6}}
    43 \newlabel{toy-intro}{{1.6}{8}{A toy compiler\relax }{subsection.1.6}{}}
    44 \@writefile{toc}{\contentsline {subsection}{\numberline {1.7}A C compiler}{8}{subsection.1.7}}
    45 \newlabel{Ccompiler-intro}{{1.7}{8}{A C compiler\relax }{subsection.1.7}{}}
    46 \@writefile{toc}{\contentsline {subsection}{\numberline {1.8}Organisation}{9}{subsection.1.8}}
    47 \@writefile{toc}{\contentsline {section}{\numberline {2}A toy compiler}{9}{section.2}}
    48 \newlabel{toy-compiler-sec}{{2}{9}{A toy compiler\relax }{section.2}{}}
    49 \@writefile{toc}{\contentsline {subsection}{\numberline {2.1}{\sf  Imp}: language and semantics}{9}{subsection.2.1}}
    50 \newlabel{imp-sec}{{2.1}{9}{\imp : language and semantics\relax }{subsection.2.1}{}}
    51 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Big-step semantics}{9}{subsection.2.2}}
    52 \citation{Leroy09-ln}
    53 \@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Big-step operational semantics of ${\sf  Imp}$}}{10}{table.1}}
    54 \newlabel{semantics-imp}{{1}{10}{Big-step operational semantics of $\imp $\relax }{table.1}{}}
    55 \@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Small-step operational semantics of ${\sf  Imp}$ commands}}{10}{table.2}}
    56 \newlabel{small-step-imp}{{2}{10}{Small-step operational semantics of $\imp $ commands\relax }{table.2}{}}
    57 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Small-step semantics}{10}{subsection.2.3}}
    58 \@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces Operational semantics ${\sf  Vm}$ programs}}{11}{table.3}}
    59 \newlabel{semantics-vm}{{3}{11}{Operational semantics $\vm $ programs\relax }{table.3}{}}
    60 \@writefile{toc}{\contentsline {subsection}{\numberline {2.4}{\sf  Vm}: language and semantics}{11}{subsection.2.4}}
    61 \newlabel{vm-sec}{{2.4}{11}{\vm : language and semantics\relax }{subsection.2.4}{}}
    62 \newlabel{unicity-height-prop}{{2}{11}{\vm : language and semantics\relax }{theorem.2}{}}
    63 \citation{Leroy09-ln}
    64 \citation{MP67}
    65 \@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Conditions for well-formed code}}{12}{table.4}}
    66 \newlabel{well-formed-instr}{{4}{12}{Conditions for well-formed code\relax }{table.4}{}}
    67 \@writefile{lot}{\contentsline {table}{\numberline {5}{\ignorespaces Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}}{12}{table.5}}
    68 \newlabel{compil-imp-vm}{{5}{12}{Compilation from $\imp $ to $\vm $\relax }{table.5}{}}
    69 \@writefile{toc}{\contentsline {subsection}{\numberline {2.5}Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}{12}{subsection.2.5}}
    70 \newlabel{compil-imp-vm-sec}{{2.5}{12}{Compilation from $\imp $ to $\vm $\relax }{subsection.2.5}{}}
    71 \@writefile{toc}{\contentsline {subsection}{\numberline {2.6}Soundness of compilation for the big-step semantics}{12}{subsection.2.6}}
    72 \newlabel{soundness-big-step-prop}{{3}{12}{Soundness of compilation for the big-step semantics\relax }{theorem.3}{}}
    73 \@writefile{toc}{\contentsline {subsection}{\numberline {2.7}Soundness of compilation for the small-step semantics}{12}{subsection.2.7}}
    74 \citation{Larus05}
    75 \newlabel{soundness-small-step}{{4}{13}{Soundness of compilation for the small-step semantics\relax }{theorem.4}{}}
    76 \@writefile{toc}{\contentsline {subsection}{\numberline {2.8}Compiled code is well-formed}{13}{subsection.2.8}}
    77 \newlabel{well-formed-prop}{{5}{13}{Compiled code is well-formed\relax }{theorem.5}{}}
    78 \@writefile{toc}{\contentsline {subsection}{\numberline {2.9}${\sf  Mips}$: language and semantics}{13}{subsection.2.9}}
    79 \newlabel{mips-sec}{{2.9}{13}{$\mips $: language and semantics\relax }{subsection.2.9}{}}
    80 \@writefile{lot}{\contentsline {table}{\numberline {6}{\ignorespaces Operational semantics ${\sf  Mips}$ programs}}{14}{table.6}}
    81 \newlabel{semantics-mips}{{6}{14}{Operational semantics $\mips $ programs\relax }{table.6}{}}
    82 \@writefile{toc}{\contentsline {subsection}{\numberline {2.10}Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}{14}{subsection.2.10}}
    83 \newlabel{compil-vm-mips-sec}{{2.10}{14}{Compilation from $\vm $ to $\mips $\relax }{subsection.2.10}{}}
    84 \newlabel{p-function}{{3}{14}{Compilation from $\vm $ to $\mips $\relax }{equation.2.3}{}}
    85 \newlabel{d-function}{{4}{14}{Compilation from $\vm $ to $\mips $\relax }{equation.2.4}{}}
    86 \newlabel{simulation-vm-mips}{{6}{14}{Compilation from $\vm $ to $\mips $\relax }{theorem.6}{}}
    87 \@writefile{toc}{\contentsline {section}{\numberline {3}Direct approach for the toy compiler}{14}{section.3}}
    88 \newlabel{toy-direct-sec}{{3}{14}{Direct approach for the toy compiler\relax }{section.3}{}}
    89 \@writefile{lot}{\contentsline {table}{\numberline {7}{\ignorespaces Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}}{15}{table.7}}
    90 \newlabel{compil-vm-mips}{{7}{15}{Compilation from $\vm $ to $\mips $\relax }{table.7}{}}
    91 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}${\sf  Mips}$ and ${\sf  Vm}$ cost annotations}{15}{subsection.3.1}}
    92 \@writefile{lot}{\contentsline {table}{\numberline {8}{\ignorespaces Upper bounds on the cost of ${\sf  Vm}$ instructions}}{16}{table.8}}
    93 \newlabel{cost-approx-instr}{{8}{16}{Upper bounds on the cost of $\vm $ instructions\relax }{table.8}{}}
    94 \newlabel{annot-vm-mips}{{7}{16}{$\mips $ and $\vm $ cost annotations\relax }{theorem.7}{}}
    95 \newlabel{labelled-simulation-vm-mips}{{8}{16}{$\mips $ and $\vm $ cost annotations\relax }{theorem.8}{}}
    96 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2}${\sf  Imp}$ cost annotation}{16}{subsection.3.2}}
    97 \newlabel{imp-cost-annotation}{{3.2}{16}{$\imp $ cost annotation\relax }{subsection.3.2}{}}
    98 \citation{Leroy09-ln}
    99 \@writefile{lot}{\contentsline {table}{\numberline {9}{\ignorespaces Annotation for ${\sf  Imp}$ programs}}{17}{table.9}}
    100 \newlabel{annotation-imp}{{9}{17}{Annotation for $\imp $ programs\relax }{table.9}{}}
    101 \newlabel{annot-imp-vm}{{9}{17}{$\imp $ cost annotation\relax }{theorem.9}{}}
    102 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Composition}{17}{subsection.3.3}}
    103 \newlabel{annot-composition}{{10}{17}{Composition\relax }{theorem.10}{}}
    104 \@writefile{toc}{\contentsline {subsection}{\numberline {3.4}${\sf  Coq}$ development}{18}{subsection.3.4}}
    105 \newlabel{coq-development-sec}{{3.4}{18}{$\coq $ development\relax }{subsection.3.4}{}}
    106 \@writefile{toc}{\contentsline {subsection}{\numberline {3.5}Limitations of the direct approach}{18}{subsection.3.5}}
    107 \newlabel{limitations-direct-sec}{{3.5}{18}{Limitations of the direct approach\relax }{subsection.3.5}{}}
    108 \@writefile{toc}{\contentsline {section}{\numberline {4}Labelling approach for the toy compiler}{18}{section.4}}
    109 \newlabel{label-toy-sec}{{4}{18}{Labelling approach for the toy compiler\relax }{section.4}{}}
    110 \@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Labelled ${\sf  Imp}$}{18}{subsection.4.1}}
    111 \@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Labelled ${\sf  Vm}$}{19}{subsection.4.2}}
    112 \newlabel{labelled-sim-imp-vm}{{11}{19}{Labelled $\vm $\relax }{theorem.11}{}}
    113 \@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Labelled ${\sf  Mips}$}{20}{subsection.4.3}}
    114 \newlabel{sim-vm-mips-prop}{{13}{20}{Labelled $\mips $\relax }{theorem.13}{}}
    115 \@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Labellings and instrumentations}{20}{subsection.4.4}}
    116 \newlabel{lab-instr-erasure-imp}{{14}{20}{Labellings and instrumentations\relax }{theorem.14}{}}
    117 \newlabel{labelling-def}{{15}{20}{Labellings and instrumentations\relax }{theorem.15}{}}
    118 \newlabel{global-commutation-prop}{{16}{20}{Labellings and instrumentations\relax }{theorem.16}{}}
    119 \newlabel{instrument-to-label-prop}{{17}{21}{Labellings and instrumentations\relax }{theorem.17}{}}
    120 \@writefile{toc}{\contentsline {subsection}{\numberline {4.5}Sound and precise labellings}{21}{subsection.4.5}}
    121 \newlabel{sound-label-sec}{{4.5}{21}{Sound and precise labellings\relax }{subsection.4.5}{}}
    122 \newlabel{sound-label-prop}{{20}{21}{Sound and precise labellings\relax }{theorem.20}{}}
    123 \newlabel{precise-label-prop}{{22}{21}{Sound and precise labellings\relax }{theorem.22}{}}
    124 \newlabel{lab-sound}{{23}{21}{Sound and precise labellings\relax }{theorem.23}{}}
    125 \@writefile{lot}{\contentsline {table}{\numberline {10}{\ignorespaces Two labellings for the ${\sf  Imp}$ language}}{22}{table.10}}
    126 \newlabel{labelling}{{10}{22}{Two labellings for the $\imp $ language\relax }{table.10}{}}
    127 \newlabel{ann-correct}{{25}{22}{Sound and precise labellings\relax }{theorem.25}{}}
    128 \citation{CIL02}
    129 \citation{Leroy09}
    130 \@writefile{toc}{\contentsline {section}{\numberline {5}A ${\sf  C}$ compiler}{23}{section.5}}
    131 \newlabel{C-compiler-sec}{{5}{23}{A $\C $ compiler\relax }{section.5}{}}
    132 \@writefile{toc}{\contentsline {subsection}{\numberline {5.1}${\sf  Clight}$}{23}{subsection.5.1}}
    133 \@writefile{toc}{\contentsline {subsection}{\numberline {5.2}${\sf  Cminor}$}{23}{subsection.5.2}}
    134 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Clight}$ to ${\sf  Cminor}$.}{23}{section*.3}}
    135 \@writefile{toc}{\contentsline {subsection}{\numberline {5.3}${\sf  RTLAbs}$}{23}{subsection.5.3}}
    136 \newlabel{syntax-clight}{{5.1}{24}{$\Clight $\relax }{subsection.5.1}{}}
    137 \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Syntax of the ${\sf  Clight}$ language}}{24}{figure.1}}
    138 \newlabel{syntax-cminor}{{5.2}{25}{$\Cminor $\relax }{subsection.5.2}{}}
    139 \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Syntax of the ${\sf  Cminor}$ language}}{25}{figure.2}}
    140 \@writefile{lot}{\contentsline {table}{\numberline {11}{\ignorespaces Syntax of the ${\sf  RTLAbs}$ language}}{26}{table.11}}
    141 \newlabel{RTLAbs:syntax}{{11}{26}{Syntax of the $\RTLAbs $ language\relax }{table.11}{}}
    142 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{26}{section*.4}}
    143 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Cminor}$ to ${\sf  RTLAbs}$.}{26}{section*.5}}
    144 \@writefile{lot}{\contentsline {table}{\numberline {12}{\ignorespaces Syntax of the ${\sf  RTL}$ language}}{27}{table.12}}
    145 \newlabel{RTL:syntax}{{12}{27}{Syntax of the $\RTL $ language\relax }{table.12}{}}
    146 \@writefile{toc}{\contentsline {subsection}{\numberline {5.4}${\sf  RTL}$}{27}{subsection.5.4}}
    147 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{27}{section*.6}}
    148 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTLAbs}$ to ${\sf  RTL}$.}{27}{section*.7}}
    149 \@writefile{toc}{\contentsline {subsection}{\numberline {5.5}${\sf  ERTL}$}{27}{subsection.5.5}}
    150 \@writefile{lot}{\contentsline {table}{\numberline {13}{\ignorespaces Syntax of the ${\sf  ERTL}$ language}}{28}{table.13}}
    151 \newlabel{ERTL:syntax}{{13}{28}{Syntax of the $\ERTL $ language\relax }{table.13}{}}
    152 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{28}{section*.8}}
    153 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTL}$ to ${\sf  ERTL}$.}{28}{section*.9}}
    154 \@writefile{toc}{\contentsline {paragraph}{Optimizations.}{28}{section*.10}}
    155 \@writefile{lot}{\contentsline {table}{\numberline {14}{\ignorespaces Syntax of the ${\sf  LTL}$ language}}{29}{table.14}}
    156 \newlabel{LTL:syntax}{{14}{29}{Syntax of the $\LTL $ language\relax }{table.14}{}}
    157 \@writefile{toc}{\contentsline {subsection}{\numberline {5.6}${\sf  LTL}$}{29}{subsection.5.6}}
    158 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{29}{section*.11}}
    159 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  ERTL}$ to ${\sf  LTL}$.}{29}{section*.12}}
    160 \@writefile{toc}{\contentsline {paragraph}{Optimizations.}{29}{section*.13}}
    161 \@writefile{lot}{\contentsline {table}{\numberline {15}{\ignorespaces Syntax of the ${\sf  LIN}$ language}}{30}{table.15}}
    162 \newlabel{LIN:syntax}{{15}{30}{Syntax of the $\LIN $ language\relax }{table.15}{}}
    163 \@writefile{toc}{\contentsline {subsection}{\numberline {5.7}${\sf  LIN}$}{30}{subsection.5.7}}
    164 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{30}{section*.14}}
    165 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LTL}$ to ${\sf  LIN}$.}{30}{section*.15}}
    166 \@writefile{toc}{\contentsline {subsection}{\numberline {5.8}${\sf  Mips}$}{30}{subsection.5.8}}
    167 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LIN}$ to ${\sf  Mips}$.}{30}{section*.16}}
    168 \@writefile{lot}{\contentsline {table}{\numberline {16}{\ignorespaces Syntax of the ${\sf  Mips}$ language}}{31}{table.16}}
    169 \newlabel{mips:syntax}{{16}{31}{Syntax of the $\mips $ language\relax }{table.16}{}}
    170 \@writefile{lot}{\contentsline {table}{\numberline {17}{\ignorespaces Building the annotation of a ${\sf  Clight}$ program in the labelling approach}}{31}{table.17}}
    171 \newlabel{annot-clight-summary}{{17}{31}{Building the annotation of a $\Clight $ program in the labelling approach\relax }{table.17}{}}
    172 \@writefile{toc}{\contentsline {section}{\numberline {6}Labelling approach for the ${\sf  C}$ compiler}{31}{section.6}}
    173 \newlabel{C-label-sec}{{6}{31}{Labelling approach for the $\C $ compiler\relax }{section.6}{}}
    174 \@writefile{toc}{\contentsline {subsection}{\numberline {6.1}Labelled ${\sf  Clight}$ and labelled ${\sf  Cminor}$}{31}{subsection.6.1}}
    175 \@writefile{toc}{\contentsline {subsection}{\numberline {6.2}Labels in ${\sf  RTLAbs}$ and the back-end languages}{32}{subsection.6.2}}
    176 \@writefile{toc}{\contentsline {subsection}{\numberline {6.3}Labelling of the source language}{32}{subsection.6.3}}
    177 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.1}Sequential instructions}{32}{subsubsection.6.3.1}}
    178 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.2}Ternary expressions}{32}{subsubsection.6.3.2}}
    179 \@writefile{toc}{\contentsline {paragraph}{Related cases.}{33}{section*.17}}
    180 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.3}Conditionals}{33}{subsubsection.6.3.3}}
    181 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.4}Loops}{33}{subsubsection.6.3.4}}
    182 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.5}Program Labels and Gotos}{34}{subsubsection.6.3.5}}
    183 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.6}Function calls}{34}{subsubsection.6.3.6}}
    184 \newlabel{fun-call-sec}{{6.3.6}{34}{Function calls\relax }{subsubsection.6.3.6}{}}
    185 \@writefile{toc}{\contentsline {subsection}{\numberline {6.4}Verifications on the object code}{35}{subsection.6.4}}
    186 \@writefile{toc}{\contentsline {subsection}{\numberline {6.5}Building the cost annotation}{35}{subsection.6.5}}
    187 \citation{Cerco10}
    188 \bibcite{AbsInt}{1}
    189 \bibcite{Cerco10}{2}
    190 \bibcite{SCADE}{3}
    191 \bibcite{Frama-C}{4}
    192 \bibcite{AbsintScade}{5}
    193 \bibcite{Fornari10}{6}
    194 \bibcite{Larus05}{7}
    195 \@writefile{toc}{\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}}
    196 \@writefile{toc}{\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}}
    197 \newlabel{conclusion-sec}{{7}{36}{Conclusion and future work\relax }{section.7}{}}
    198 \bibcite{Leroy09}{8}
    199 \bibcite{Leroy09-ln}{9}
    200 \bibcite{MP67}{10}
    201 \bibcite{CIL02}{11}
    202 \bibcite{Pottier}{12}
    203 \bibcite{W09}{13}
    204 \@writefile{toc}{\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}}
    205 \@writefile{toc}{\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}}
    206 \newlabel{paper-proofs}{{B}{40}{Proofs\relax }{appendix.B}{}}
    207 \@writefile{toc}{\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}}
    208 \@writefile{toc}{\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref  {soundness-small-step}}{40}{subsection.B.2}}
    209 \newlabel{access-lemma}{{26}{40}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.26}{}}
    210 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref  {labelled-simulation-vm-mips}}{41}{subsection.B.3}}
    211 \newlabel{step1}{{7}{41}{Proof of proposition \ref {labelled-simulation-vm-mips}\relax }{equation.B.7}{}}
    212 \@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{41}{section*.19}}
    213 \@writefile{toc}{\contentsline {paragraph}{The inequation.}{41}{section*.20}}
    214 \@writefile{toc}{\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref  {annot-composition}}{41}{subsection.B.4}}
    215 \@writefile{toc}{\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref  {labelled-sim-imp-vm}}{42}{subsection.B.5}}
    216 \@writefile{toc}{\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref  {sim-vm-mips-prop}}{42}{subsection.B.6}}
    217 \@writefile{toc}{\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref  {lab-instr-erasure-imp}}{42}{subsection.B.7}}
    218 \@writefile{toc}{\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref  {global-commutation-prop}}{42}{subsection.B.8}}
    219 \@writefile{toc}{\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref  {instrument-to-label-prop}}{42}{subsection.B.9}}
    220 \@writefile{toc}{\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref  {sound-label-prop}}{43}{subsection.B.10}}
    221 \@writefile{toc}{\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref  {precise-label-prop}}{43}{subsection.B.11}}
    222 \@writefile{toc}{\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref  {lab-sound}}{43}{subsection.B.12}}
    223 \newlabel{precise-lemma}{{29}{43}{Proof of proposition \ref {lab-sound}\relax }{theorem.29}{}}
    224 \@writefile{toc}{\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref  {ann-correct}}{43}{subsection.B.13}}
     28\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{4}{section.1}}
     29\newlabel{intro-sec}{{1}{4}{Introduction\relax }{section.1}{}}
     30\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Meaning of cost annotations}{4}{subsection.1.1}}
Note: See TracChangeset for help on using the changeset viewer.