Ignore:
Timestamp:
Sep 10, 2010, 3:51:04 PM (9 years ago)
Author:
sacerdot
Message:

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

File:
1 edited

Legend:

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

    r39 r59  
    202202\bibcite{Pottier}{12}
    203203\bibcite{W09}{13}
    204 \@writefile{toc}{\contentsline {section}{\numberline {A}Proofs}{38}{appendix.A}}
    205 \newlabel{paper-proofs}{{A}{38}{Proofs\relax }{appendix.A}{}}
    206 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1}Notation}{38}{subsection.A.1}}
    207 \@writefile{toc}{\contentsline {subsection}{\numberline {A.2}Proof of proposition \ref  {soundness-small-step}}{38}{subsection.A.2}}
    208 \newlabel{access-lemma}{{26}{38}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.26}{}}
    209 \@writefile{toc}{\contentsline {subsection}{\numberline {A.3}Proof of proposition \ref  {labelled-simulation-vm-mips}}{39}{subsection.A.3}}
    210 \newlabel{step1}{{7}{39}{Proof of proposition \ref {labelled-simulation-vm-mips}\relax }{equation.A.7}{}}
    211 \@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{39}{section*.19}}
    212 \@writefile{toc}{\contentsline {paragraph}{The inequation.}{39}{section*.20}}
    213 \@writefile{toc}{\contentsline {subsection}{\numberline {A.4}Proof of proposition \ref  {annot-composition}}{39}{subsection.A.4}}
    214 \@writefile{toc}{\contentsline {subsection}{\numberline {A.5}Proof of proposition \ref  {labelled-sim-imp-vm}}{40}{subsection.A.5}}
    215 \@writefile{toc}{\contentsline {subsection}{\numberline {A.6}Proof of proposition \ref  {sim-vm-mips-prop}}{40}{subsection.A.6}}
    216 \@writefile{toc}{\contentsline {subsection}{\numberline {A.7}Proof of proposition \ref  {lab-instr-erasure-imp}}{40}{subsection.A.7}}
    217 \@writefile{toc}{\contentsline {subsection}{\numberline {A.8}Proof of proposition \ref  {global-commutation-prop}}{40}{subsection.A.8}}
    218 \@writefile{toc}{\contentsline {subsection}{\numberline {A.9}Proof of proposition \ref  {instrument-to-label-prop}}{40}{subsection.A.9}}
    219 \@writefile{toc}{\contentsline {subsection}{\numberline {A.10}Proof of proposition \ref  {sound-label-prop}}{41}{subsection.A.10}}
    220 \@writefile{toc}{\contentsline {subsection}{\numberline {A.11}Proof of proposition \ref  {precise-label-prop}}{41}{subsection.A.11}}
    221 \@writefile{toc}{\contentsline {subsection}{\numberline {A.12}Proof of proposition \ref  {lab-sound}}{41}{subsection.A.12}}
    222 \newlabel{precise-lemma}{{29}{41}{Proof of proposition \ref {lab-sound}\relax }{theorem.29}{}}
    223 \@writefile{toc}{\contentsline {subsection}{\numberline {A.13}Proof of proposition \ref  {ann-correct}}{41}{subsection.A.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 TracChangeset for help on using the changeset viewer.