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

    r59 r1982  
    11\BOOKMARK [1][]{section.1}{Introduction}{}
    22\BOOKMARK [2][]{subsection.1.1}{Meaning of cost annotations}{section.1}
    3 \BOOKMARK [2][]{subsection.1.2}{Soundness and precision of cost annotations}{section.1}
    4 \BOOKMARK [2][]{subsection.1.3}{Compositionality}{section.1}
    5 \BOOKMARK [2][]{subsection.1.4}{Direct approach to cost annotations}{section.1}
    6 \BOOKMARK [2][]{subsection.1.5}{Labelling approach to cost annotations}{section.1}
    7 \BOOKMARK [2][]{subsection.1.6}{A toy compiler}{section.1}
    8 \BOOKMARK [2][]{subsection.1.7}{A C compiler}{section.1}
    9 \BOOKMARK [2][]{subsection.1.8}{Organisation}{section.1}
    10 \BOOKMARK [1][]{section.2}{A toy compiler}{}
    11 \BOOKMARK [2][]{subsection.2.1}{Imp: language and semantics}{section.2}
    12 \BOOKMARK [2][]{subsection.2.2}{Big-step semantics}{section.2}
    13 \BOOKMARK [2][]{subsection.2.3}{Small-step semantics}{section.2}
    14 \BOOKMARK [2][]{subsection.2.4}{Vm: language and semantics}{section.2}
    15 \BOOKMARK [2][]{subsection.2.5}{Compilation from Imp to Vm}{section.2}
    16 \BOOKMARK [2][]{subsection.2.6}{Soundness of compilation for the big-step semantics}{section.2}
    17 \BOOKMARK [2][]{subsection.2.7}{Soundness of compilation for the small-step semantics}{section.2}
    18 \BOOKMARK [2][]{subsection.2.8}{Compiled code is well-formed}{section.2}
    19 \BOOKMARK [2][]{subsection.2.9}{Mips: language and semantics}{section.2}
    20 \BOOKMARK [2][]{subsection.2.10}{Compilation from Vm to Mips}{section.2}
    21 \BOOKMARK [1][]{section.3}{Direct approach for the toy compiler}{}
    22 \BOOKMARK [2][]{subsection.3.1}{Mips and Vm cost annotations}{section.3}
    23 \BOOKMARK [2][]{subsection.3.2}{Imp cost annotation}{section.3}
    24 \BOOKMARK [2][]{subsection.3.3}{Composition}{section.3}
    25 \BOOKMARK [2][]{subsection.3.4}{Coq development}{section.3}
    26 \BOOKMARK [2][]{subsection.3.5}{Limitations of the direct approach}{section.3}
    27 \BOOKMARK [1][]{section.4}{Labelling approach for the toy compiler}{}
    28 \BOOKMARK [2][]{subsection.4.1}{Labelled Imp}{section.4}
    29 \BOOKMARK [2][]{subsection.4.2}{Labelled Vm}{section.4}
    30 \BOOKMARK [2][]{subsection.4.3}{Labelled Mips}{section.4}
    31 \BOOKMARK [2][]{subsection.4.4}{Labellings and instrumentations}{section.4}
    32 \BOOKMARK [2][]{subsection.4.5}{Sound and precise labellings}{section.4}
    33 \BOOKMARK [1][]{section.5}{A C compiler}{}
    34 \BOOKMARK [2][]{subsection.5.1}{Clight}{section.5}
    35 \BOOKMARK [2][]{subsection.5.2}{Cminor}{section.5}
    36 \BOOKMARK [2][]{subsection.5.3}{RTLAbs}{section.5}
    37 \BOOKMARK [2][]{subsection.5.4}{RTL}{section.5}
    38 \BOOKMARK [2][]{subsection.5.5}{ERTL}{section.5}
    39 \BOOKMARK [2][]{subsection.5.6}{LTL}{section.5}
    40 \BOOKMARK [2][]{subsection.5.7}{LIN}{section.5}
    41 \BOOKMARK [2][]{subsection.5.8}{Mips}{section.5}
    42 \BOOKMARK [1][]{section.6}{Labelling approach for the C compiler}{}
    43 \BOOKMARK [2][]{subsection.6.1}{Labelled Clight and labelled Cminor}{section.6}
    44 \BOOKMARK [2][]{subsection.6.2}{Labels in RTLAbs and the back-end languages}{section.6}
    45 \BOOKMARK [2][]{subsection.6.3}{Labelling of the source language}{section.6}
    46 \BOOKMARK [3][]{subsubsection.6.3.1}{Sequential instructions}{subsection.6.3}
    47 \BOOKMARK [3][]{subsubsection.6.3.2}{Ternary expressions}{subsection.6.3}
    48 \BOOKMARK [3][]{subsubsection.6.3.3}{Conditionals}{subsection.6.3}
    49 \BOOKMARK [3][]{subsubsection.6.3.4}{Loops}{subsection.6.3}
    50 \BOOKMARK [3][]{subsubsection.6.3.5}{Program Labels and Gotos}{subsection.6.3}
    51 \BOOKMARK [3][]{subsubsection.6.3.6}{Function calls}{subsection.6.3}
    52 \BOOKMARK [2][]{subsection.6.4}{Verifications on the object code}{section.6}
    53 \BOOKMARK [2][]{subsection.6.5}{Building the cost annotation}{section.6}
    54 \BOOKMARK [2][]{subsection.6.6}{Testing}{section.6}
    55 \BOOKMARK [1][]{section.7}{Conclusion and future work}{}
    56 \BOOKMARK [1][]{appendix.A}{Assessment of the deliverable within the CerCo project}{}
    57 \BOOKMARK [1][]{appendix.B}{Proofs}{}
    58 \BOOKMARK [2][]{subsection.B.1}{Notation}{appendix.B}
    59 \BOOKMARK [2][]{subsection.B.2}{Proof of proposition 4}{appendix.B}
    60 \BOOKMARK [2][]{subsection.B.3}{Proof of proposition 8}{appendix.B}
    61 \BOOKMARK [2][]{subsection.B.4}{Proof of proposition 10}{appendix.B}
    62 \BOOKMARK [2][]{subsection.B.5}{Proof of proposition 11}{appendix.B}
    63 \BOOKMARK [2][]{subsection.B.6}{Proof of proposition 13}{appendix.B}
    64 \BOOKMARK [2][]{subsection.B.7}{Proof of proposition 14}{appendix.B}
    65 \BOOKMARK [2][]{subsection.B.8}{Proof of proposition 16}{appendix.B}
    66 \BOOKMARK [2][]{subsection.B.9}{Proof of proposition 17}{appendix.B}
    67 \BOOKMARK [2][]{subsection.B.10}{Proof of proposition 20}{appendix.B}
    68 \BOOKMARK [2][]{subsection.B.11}{Proof of proposition 22}{appendix.B}
    69 \BOOKMARK [2][]{subsection.B.12}{Proof of proposition 23}{appendix.B}
    70 \BOOKMARK [2][]{subsection.B.13}{Proof of proposition 25}{appendix.B}
Note: See TracChangeset for help on using the changeset viewer.