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.toc

    r39 r59  
    7171\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}
    7272\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}
    73 \contentsline {section}{\numberline {A}Proofs}{38}{appendix.A}
    74 \contentsline {subsection}{\numberline {A.1}Notation}{38}{subsection.A.1}
    75 \contentsline {subsection}{\numberline {A.2}Proof of proposition \ref {soundness-small-step}}{38}{subsection.A.2}
    76 \contentsline {subsection}{\numberline {A.3}Proof of proposition \ref {labelled-simulation-vm-mips}}{39}{subsection.A.3}
    77 \contentsline {paragraph}{The memory realisation.}{39}{section*.19}
    78 \contentsline {paragraph}{The inequation.}{39}{section*.20}
    79 \contentsline {subsection}{\numberline {A.4}Proof of proposition \ref {annot-composition}}{39}{subsection.A.4}
    80 \contentsline {subsection}{\numberline {A.5}Proof of proposition \ref {labelled-sim-imp-vm}}{40}{subsection.A.5}
    81 \contentsline {subsection}{\numberline {A.6}Proof of proposition \ref {sim-vm-mips-prop}}{40}{subsection.A.6}
    82 \contentsline {subsection}{\numberline {A.7}Proof of proposition \ref {lab-instr-erasure-imp}}{40}{subsection.A.7}
    83 \contentsline {subsection}{\numberline {A.8}Proof of proposition \ref {global-commutation-prop}}{40}{subsection.A.8}
    84 \contentsline {subsection}{\numberline {A.9}Proof of proposition \ref {instrument-to-label-prop}}{40}{subsection.A.9}
    85 \contentsline {subsection}{\numberline {A.10}Proof of proposition \ref {sound-label-prop}}{41}{subsection.A.10}
    86 \contentsline {subsection}{\numberline {A.11}Proof of proposition \ref {precise-label-prop}}{41}{subsection.A.11}
    87 \contentsline {subsection}{\numberline {A.12}Proof of proposition \ref {lab-sound}}{41}{subsection.A.12}
    88 \contentsline {subsection}{\numberline {A.13}Proof of proposition \ref {ann-correct}}{41}{subsection.A.13}
     73\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}
     74\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}
     75\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}
     76\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {soundness-small-step}}{40}{subsection.B.2}
     77\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {labelled-simulation-vm-mips}}{41}{subsection.B.3}
     78\contentsline {paragraph}{The memory realisation.}{41}{section*.19}
     79\contentsline {paragraph}{The inequation.}{41}{section*.20}
     80\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {annot-composition}}{41}{subsection.B.4}
     81\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {labelled-sim-imp-vm}}{42}{subsection.B.5}
     82\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {sim-vm-mips-prop}}{42}{subsection.B.6}
     83\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {lab-instr-erasure-imp}}{42}{subsection.B.7}
     84\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {global-commutation-prop}}{42}{subsection.B.8}
     85\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {instrument-to-label-prop}}{42}{subsection.B.9}
     86\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {sound-label-prop}}{43}{subsection.B.10}
     87\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {precise-label-prop}}{43}{subsection.B.11}
     88\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref {lab-sound}}{43}{subsection.B.12}
     89\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.