Changeset 3615


Ignore:
Timestamp:
Mar 6, 2017, 3:31:01 PM (3 years ago)
Author:
boender
Message:

Moved paper structure comments to their relevant sections

Location:
Papers/jar-cerco-2017
Files:
7 edited

Legend:

Unmodified
Added
Removed

  • Papers/jar-cerco-2017/architecture.tex

    r3613 r3615  
     1% CerCo compiler architecture
     2%   Description of languages
     3%   Target hardware description
     4
    15\section{Compiler architecture}
    26\label{sect.compiler.architecture}

  • Papers/jar-cerco-2017/cerco.tex

    r3614 r3615  
    6363\smartqed
    6464
    65 % PROPOSED PAPER STRUCTURE
    66 
    67 % Introduction
    68 %   Problem being solved, background, etc.
    69 %   Current state of the art (and problem with it)
    70 %   The `CerCo approach' (tm)
    71 %   Brief Matita overview
    72 %   Map of paper
    73 
    74 % CerCo compiler architecture
    75 %   Description of languages
    76 %   Target hardware description
    77 
    78 % Compiler proof
    79 %   Structure of proof, and high-level discussion
    80 %   Technical devices: structured traces, labelling, etc.
    81 %   Assembler proof
    82 %   Technical issues in front end (Brian?)
    83 %   Main theorem statement
    84 
    85 % FramaC plugin
    86 %   Purpose
    87 %   Description of architecture
    88 %   Case study/worked example (crypto example?)
    89 
    90 % Formal development
    91 %   Source code repo link
    92 %   Statistics (number of lines, etc.)
    93 %   Description of remaining axioms --- try and explain them away/make them sound reasonable
    94 
    95 % Conclusions
    96 %   Summary
    97 %   Related work
    98 %   Future work
    99 
    100 % Bibliography
    101 
    10265\title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the
    10366financial support of the Future and Emerging Technologies (FET) programme within

  • Papers/jar-cerco-2017/conclusions.tex

    r3613 r3615  
    1 \section{Conclusions}
    2 \label{sect.conclusions}
    3 
     1% Conclusions
    42%   Summary
    53%   Related work
    64%   Future work
     5
     6\section{Conclusions}
     7\label{sect.conclusions}
    78
    89In many application domains the intensional properties of programs---time and space usage, for example---are an important factor in the specification of a program, and therefore overall program correctness.

  • Papers/jar-cerco-2017/development.tex

    r3613 r3615  
     1% Formal development
     2%   Source code repo link
     3%   Statistics (number of lines, etc.)
     4%   Description of remaining axioms --- try and explain them away/make them sound reasonable
     5
    16\section{Formal development}
    27\label{sect.formal.development}
    3 

  • Papers/jar-cerco-2017/framac.tex

    r3613 r3615  
     1% FramaC plugin
     2%   Purpose
     3%   Description of architecture
     4%   Case study/worked example (crypto example?)
     5
    16\section{FramaC plugin}
    27\label{sect.framac.plugin}

  • Papers/jar-cerco-2017/introduction.tex

    r3614 r3615  
     1% Introduction
     2%   Problem being solved, background, etc.
     3%   Current state of the art (and problem with it)
     4%   The `CerCo approach' (tm)
     5%   Brief Matita overview
     6%   Map of paper
     7
    18\section{Introduction}
    29\label{sect.introduction}

  • Papers/jar-cerco-2017/proof.tex

    r3613 r3615  
     1% Compiler proof
     2%   Structure of proof, and high-level discussion
     3%   Technical devices: structured traces, labelling, etc.
     4%   Assembler proof
     5%   Technical issues in front end (Brian?)
     6%   Main theorem statement
     7
    18\section{Compiler proof}
    29\label{sect.compiler.proof}
Note: See TracChangeset for help on using the changeset viewer.