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

Last change on this file since 59 was 59, checked in by sacerdot, 9 years ago

Added a new appendix for assessment within the CerCo? project.

File size: 18.8 KB
Line 
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 {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}}
Note: See TracBrowser for help on using the repository browser.