source: Deliverables/D2.1/report.aux @ 162

\relax 
\ifx\hyper@anchor\@undefined
\global \let \oldcontentsline\contentsline
\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global \let \oldnewlabel\newlabel
\gdef \newlabel#1#2{\newlabelxx{#1}#2}
\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\let \contentsline\oldcontentsline
\let \newlabel\oldnewlabel}
\else
\global \let \hyper@last\relax 
\fi

\bibstyle{abbrv}
\select@language{english}
\@writefile{toc}{\select@language{english}}
\@writefile{lof}{\select@language{english}}
\@writefile{lot}{\select@language{english}}
\@writefile{toc}{\contentsline {paragraph}{Abstract}{2}{section*.1}}
\citation{Leroy09}
\citation{Cerco10}
\citation{SCADE}
\citation{Fornari10}
\citation{AbsInt}
\citation{AbsintScade}
\citation{W09}
\citation{Frama-C}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{5}{section.1}}
\newlabel{intro-sec}{{1}{5}{Introduction\relax }{section.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Meaning of cost annotations}{5}{subsection.1.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Soundness and precision of cost annotations}{6}{subsection.1.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Compositionality}{6}{subsection.1.3}}
\newlabel{comp-intro}{{1.3}{6}{Compositionality\relax }{subsection.1.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4}Direct approach to cost annotations}{6}{subsection.1.4}}
\newlabel{direct-intro}{{1.4}{6}{Direct approach to cost annotations\relax }{subsection.1.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.5}Labelling approach to cost annotations}{7}{subsection.1.5}}
\newlabel{label-intro}{{1.5}{7}{Labelling approach to cost annotations\relax }{subsection.1.5}{}}
\newlabel{STEP1}{{1}{7}{Labelling approach to cost annotations\relax }{equation.1.1}{}}
\citation{CIL02}
\citation{Pottier}
\newlabel{step2}{{2}{8}{Labelling approach to cost annotations\relax }{equation.1.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.6}A toy compiler}{8}{subsection.1.6}}
\newlabel{toy-intro}{{1.6}{8}{A toy compiler\relax }{subsection.1.6}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.7}A C compiler}{8}{subsection.1.7}}
\newlabel{Ccompiler-intro}{{1.7}{8}{A C compiler\relax }{subsection.1.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.8}Organisation}{9}{subsection.1.8}}
\@writefile{toc}{\contentsline {section}{\numberline {2}A toy compiler}{9}{section.2}}
\newlabel{toy-compiler-sec}{{2}{9}{A toy compiler\relax }{section.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}{\sf  Imp}: language and semantics}{9}{subsection.2.1}}
\newlabel{imp-sec}{{2.1}{9}{\imp : language and semantics\relax }{subsection.2.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Big-step semantics}{9}{subsection.2.2}}
\citation{Leroy09-ln}
\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Big-step operational semantics of ${\sf  Imp}$}}{10}{table.1}}
\newlabel{semantics-imp}{{1}{10}{Big-step operational semantics of $\imp $\relax }{table.1}{}}
\@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Small-step operational semantics of ${\sf  Imp}$ commands}}{10}{table.2}}
\newlabel{small-step-imp}{{2}{10}{Small-step operational semantics of $\imp $ commands\relax }{table.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Small-step semantics}{10}{subsection.2.3}}
\@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces Operational semantics ${\sf  Vm}$ programs}}{11}{table.3}}
\newlabel{semantics-vm}{{3}{11}{Operational semantics $\vm $ programs\relax }{table.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4}{\sf  Vm}: language and semantics}{11}{subsection.2.4}}
\newlabel{vm-sec}{{2.4}{11}{\vm : language and semantics\relax }{subsection.2.4}{}}
\newlabel{unicity-height-prop}{{2}{11}{\vm : language and semantics\relax }{theorem.2}{}}
\citation{Leroy09-ln}
\citation{MP67}
\@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Conditions for well-formed code}}{12}{table.4}}
\newlabel{well-formed-instr}{{4}{12}{Conditions for well-formed code\relax }{table.4}{}}
\@writefile{lot}{\contentsline {table}{\numberline {5}{\ignorespaces Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}}{12}{table.5}}
\newlabel{compil-imp-vm}{{5}{12}{Compilation from $\imp $ to $\vm $\relax }{table.5}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.5}Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}{12}{subsection.2.5}}
\newlabel{compil-imp-vm-sec}{{2.5}{12}{Compilation from $\imp $ to $\vm $\relax }{subsection.2.5}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.6}Soundness of compilation for the big-step semantics}{12}{subsection.2.6}}
\newlabel{soundness-big-step-prop}{{3}{12}{Soundness of compilation for the big-step semantics\relax }{theorem.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.7}Soundness of compilation for the small-step semantics}{12}{subsection.2.7}}
\citation{Larus05}
\newlabel{soundness-small-step}{{4}{13}{Soundness of compilation for the small-step semantics\relax }{theorem.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.8}Compiled code is well-formed}{13}{subsection.2.8}}
\newlabel{well-formed-prop}{{5}{13}{Compiled code is well-formed\relax }{theorem.5}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.9}${\sf  Mips}$: language and semantics}{13}{subsection.2.9}}
\newlabel{mips-sec}{{2.9}{13}{$\mips $: language and semantics\relax }{subsection.2.9}{}}
\@writefile{lot}{\contentsline {table}{\numberline {6}{\ignorespaces Operational semantics ${\sf  Mips}$ programs}}{14}{table.6}}
\newlabel{semantics-mips}{{6}{14}{Operational semantics $\mips $ programs\relax }{table.6}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.10}Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}{14}{subsection.2.10}}
\newlabel{compil-vm-mips-sec}{{2.10}{14}{Compilation from $\vm $ to $\mips $\relax }{subsection.2.10}{}}
\newlabel{p-function}{{3}{14}{Compilation from $\vm $ to $\mips $\relax }{equation.2.3}{}}
\newlabel{d-function}{{4}{14}{Compilation from $\vm $ to $\mips $\relax }{equation.2.4}{}}
\newlabel{simulation-vm-mips}{{6}{14}{Compilation from $\vm $ to $\mips $\relax }{theorem.6}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Direct approach for the toy compiler}{14}{section.3}}
\newlabel{toy-direct-sec}{{3}{14}{Direct approach for the toy compiler\relax }{section.3}{}}
\@writefile{lot}{\contentsline {table}{\numberline {7}{\ignorespaces Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}}{15}{table.7}}
\newlabel{compil-vm-mips}{{7}{15}{Compilation from $\vm $ to $\mips $\relax }{table.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}${\sf  Mips}$ and ${\sf  Vm}$ cost annotations}{15}{subsection.3.1}}
\@writefile{lot}{\contentsline {table}{\numberline {8}{\ignorespaces Upper bounds on the cost of ${\sf  Vm}$ instructions}}{16}{table.8}}
\newlabel{cost-approx-instr}{{8}{16}{Upper bounds on the cost of $\vm $ instructions\relax }{table.8}{}}
\newlabel{annot-vm-mips}{{7}{16}{$\mips $ and $\vm $ cost annotations\relax }{theorem.7}{}}
\newlabel{labelled-simulation-vm-mips}{{8}{16}{$\mips $ and $\vm $ cost annotations\relax }{theorem.8}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}${\sf  Imp}$ cost annotation}{16}{subsection.3.2}}
\newlabel{imp-cost-annotation}{{3.2}{16}{$\imp $ cost annotation\relax }{subsection.3.2}{}}
\citation{Leroy09-ln}
\@writefile{lot}{\contentsline {table}{\numberline {9}{\ignorespaces Annotation for ${\sf  Imp}$ programs}}{17}{table.9}}
\newlabel{annotation-imp}{{9}{17}{Annotation for $\imp $ programs\relax }{table.9}{}}
\newlabel{annot-imp-vm}{{9}{17}{$\imp $ cost annotation\relax }{theorem.9}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Composition}{17}{subsection.3.3}}
\newlabel{annot-composition}{{10}{17}{Composition\relax }{theorem.10}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}${\sf  Coq}$ development}{18}{subsection.3.4}}
\newlabel{coq-development-sec}{{3.4}{18}{$\coq $ development\relax }{subsection.3.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.5}Limitations of the direct approach}{18}{subsection.3.5}}
\newlabel{limitations-direct-sec}{{3.5}{18}{Limitations of the direct approach\relax }{subsection.3.5}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Labelling approach for the toy compiler}{18}{section.4}}
\newlabel{label-toy-sec}{{4}{18}{Labelling approach for the toy compiler\relax }{section.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Labelled ${\sf  Imp}$}{18}{subsection.4.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Labelled ${\sf  Vm}$}{19}{subsection.4.2}}
\newlabel{labelled-sim-imp-vm}{{11}{19}{Labelled $\vm $\relax }{theorem.11}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Labelled ${\sf  Mips}$}{20}{subsection.4.3}}
\newlabel{sim-vm-mips-prop}{{13}{20}{Labelled $\mips $\relax }{theorem.13}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Labellings and instrumentations}{20}{subsection.4.4}}
\newlabel{lab-instr-erasure-imp}{{14}{20}{Labellings and instrumentations\relax }{theorem.14}{}}
\newlabel{labelling-def}{{15}{20}{Labellings and instrumentations\relax }{theorem.15}{}}
\newlabel{global-commutation-prop}{{16}{20}{Labellings and instrumentations\relax }{theorem.16}{}}
\newlabel{instrument-to-label-prop}{{17}{21}{Labellings and instrumentations\relax }{theorem.17}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.5}Sound and precise labellings}{21}{subsection.4.5}}
\newlabel{sound-label-sec}{{4.5}{21}{Sound and precise labellings\relax }{subsection.4.5}{}}
\newlabel{sound-label-prop}{{20}{21}{Sound and precise labellings\relax }{theorem.20}{}}
\newlabel{precise-label-prop}{{22}{21}{Sound and precise labellings\relax }{theorem.22}{}}
\newlabel{lab-sound}{{23}{21}{Sound and precise labellings\relax }{theorem.23}{}}
\@writefile{lot}{\contentsline {table}{\numberline {10}{\ignorespaces Two labellings for the ${\sf  Imp}$ language}}{22}{table.10}}
\newlabel{labelling}{{10}{22}{Two labellings for the $\imp $ language\relax }{table.10}{}}
\newlabel{ann-correct}{{25}{22}{Sound and precise labellings\relax }{theorem.25}{}}
\citation{CIL02}
\citation{Leroy09}
\@writefile{toc}{\contentsline {section}{\numberline {5}A ${\sf  C}$ compiler}{23}{section.5}}
\newlabel{C-compiler-sec}{{5}{23}{A $\C $ compiler\relax }{section.5}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}${\sf  Clight}$}{23}{subsection.5.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}${\sf  Cminor}$}{23}{subsection.5.2}}
\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Clight}$ to ${\sf  Cminor}$.}{23}{section*.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}${\sf  RTLAbs}$}{23}{subsection.5.3}}
\newlabel{syntax-clight}{{5.1}{24}{$\Clight $\relax }{subsection.5.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Syntax of the ${\sf  Clight}$ language}}{24}{figure.1}}
\newlabel{syntax-cminor}{{5.2}{25}{$\Cminor $\relax }{subsection.5.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Syntax of the ${\sf  Cminor}$ language}}{25}{figure.2}}
\@writefile{lot}{\contentsline {table}{\numberline {11}{\ignorespaces Syntax of the ${\sf  RTLAbs}$ language}}{26}{table.11}}
\newlabel{RTLAbs:syntax}{{11}{26}{Syntax of the $\RTLAbs $ language\relax }{table.11}{}}
\@writefile{toc}{\contentsline {paragraph}{Syntax.}{26}{section*.4}}
\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Cminor}$ to ${\sf  RTLAbs}$.}{26}{section*.5}}
\@writefile{lot}{\contentsline {table}{\numberline {12}{\ignorespaces Syntax of the ${\sf  RTL}$ language}}{27}{table.12}}
\newlabel{RTL:syntax}{{12}{27}{Syntax of the $\RTL $ language\relax }{table.12}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}${\sf  RTL}$}{27}{subsection.5.4}}
\@writefile{toc}{\contentsline {paragraph}{Syntax.}{27}{section*.6}}
\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTLAbs}$ to ${\sf  RTL}$.}{27}{section*.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5}${\sf  ERTL}$}{27}{subsection.5.5}}
\@writefile{lot}{\contentsline {table}{\numberline {13}{\ignorespaces Syntax of the ${\sf  ERTL}$ language}}{28}{table.13}}
\newlabel{ERTL:syntax}{{13}{28}{Syntax of the $\ERTL $ language\relax }{table.13}{}}
\@writefile{toc}{\contentsline {paragraph}{Syntax.}{28}{section*.8}}
\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTL}$ to ${\sf  ERTL}$.}{28}{section*.9}}
\@writefile{toc}{\contentsline {paragraph}{Optimizations.}{28}{section*.10}}
\@writefile{lot}{\contentsline {table}{\numberline {14}{\ignorespaces Syntax of the ${\sf  LTL}$ language}}{29}{table.14}}
\newlabel{LTL:syntax}{{14}{29}{Syntax of the $\LTL $ language\relax }{table.14}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6}${\sf  LTL}$}{29}{subsection.5.6}}
\@writefile{toc}{\contentsline {paragraph}{Syntax.}{29}{section*.11}}
\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  ERTL}$ to ${\sf  LTL}$.}{29}{section*.12}}
\@writefile{toc}{\contentsline {paragraph}{Optimizations.}{29}{section*.13}}
\@writefile{lot}{\contentsline {table}{\numberline {15}{\ignorespaces Syntax of the ${\sf  LIN}$ language}}{30}{table.15}}
\newlabel{LIN:syntax}{{15}{30}{Syntax of the $\LIN $ language\relax }{table.15}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.7}${\sf  LIN}$}{30}{subsection.5.7}}
\@writefile{toc}{\contentsline {paragraph}{Syntax.}{30}{section*.14}}
\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LTL}$ to ${\sf  LIN}$.}{30}{section*.15}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.8}${\sf  Mips}$}{30}{subsection.5.8}}
\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LIN}$ to ${\sf  Mips}$.}{30}{section*.16}}
\@writefile{lot}{\contentsline {table}{\numberline {16}{\ignorespaces Syntax of the ${\sf  Mips}$ language}}{31}{table.16}}
\newlabel{mips:syntax}{{16}{31}{Syntax of the $\mips $ language\relax }{table.16}{}}
\@writefile{lot}{\contentsline {table}{\numberline {17}{\ignorespaces Building the annotation of a ${\sf  Clight}$ program in the labelling approach}}{31}{table.17}}
\newlabel{annot-clight-summary}{{17}{31}{Building the annotation of a $\Clight $ program in the labelling approach\relax }{table.17}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Labelling approach for the ${\sf  C}$ compiler}{31}{section.6}}
\newlabel{C-label-sec}{{6}{31}{Labelling approach for the $\C $ compiler\relax }{section.6}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.1}Labelled ${\sf  Clight}$ and labelled ${\sf  Cminor}$}{31}{subsection.6.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.2}Labels in ${\sf  RTLAbs}$ and the back-end languages}{32}{subsection.6.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.3}Labelling of the source language}{32}{subsection.6.3}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.1}Sequential instructions}{32}{subsubsection.6.3.1}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.2}Ternary expressions}{32}{subsubsection.6.3.2}}
\@writefile{toc}{\contentsline {paragraph}{Related cases.}{33}{section*.17}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.3}Conditionals}{33}{subsubsection.6.3.3}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.4}Loops}{33}{subsubsection.6.3.4}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.5}Program Labels and Gotos}{34}{subsubsection.6.3.5}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.6}Function calls}{34}{subsubsection.6.3.6}}
\newlabel{fun-call-sec}{{6.3.6}{34}{Function calls\relax }{subsubsection.6.3.6}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.4}Verifications on the object code}{35}{subsection.6.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.5}Building the cost annotation}{35}{subsection.6.5}}
\citation{Cerco10}
\bibcite{AbsInt}{1}
\bibcite{Cerco10}{2}
\bibcite{SCADE}{3}
\bibcite{Frama-C}{4}
\bibcite{AbsintScade}{5}
\bibcite{Fornari10}{6}
\bibcite{Larus05}{7}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}}
\newlabel{conclusion-sec}{{7}{36}{Conclusion and future work\relax }{section.7}{}}
\bibcite{Leroy09}{8}
\bibcite{Leroy09-ln}{9}
\bibcite{MP67}{10}
\bibcite{CIL02}{11}
\bibcite{Pottier}{12}
\bibcite{W09}{13}
\@writefile{toc}{\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}}
\@writefile{toc}{\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}}
\newlabel{paper-proofs}{{B}{40}{Proofs\relax }{appendix.B}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref  {soundness-small-step}}{40}{subsection.B.2}}
\newlabel{access-lemma}{{26}{40}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.26}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref  {labelled-simulation-vm-mips}}{41}{subsection.B.3}}
\newlabel{step1}{{7}{41}{Proof of proposition \ref {labelled-simulation-vm-mips}\relax }{equation.B.7}{}}
\@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{41}{section*.19}}
\@writefile{toc}{\contentsline {paragraph}{The inequation.}{41}{section*.20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref  {annot-composition}}{41}{subsection.B.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref  {labelled-sim-imp-vm}}{42}{subsection.B.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref  {sim-vm-mips-prop}}{42}{subsection.B.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref  {lab-instr-erasure-imp}}{42}{subsection.B.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref  {global-commutation-prop}}{42}{subsection.B.8}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref  {instrument-to-label-prop}}{42}{subsection.B.9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref  {sound-label-prop}}{43}{subsection.B.10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref  {precise-label-prop}}{43}{subsection.B.11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref  {lab-sound}}{43}{subsection.B.12}}
\newlabel{precise-lemma}{{29}{43}{Proof of proposition \ref {lab-sound}\relax }{theorem.29}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref  {ann-correct}}{43}{subsection.B.13}}