Changeset 3615
- Timestamp:
- Mar 6, 2017, 3:31:01 PM (4 years ago)
- 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 1 5 \section{Compiler architecture} 2 6 \label{sect.compiler.architecture} -
Papers/jar-cerco-2017/cerco.tex
r3614 r3615 63 63 \smartqed 64 64 65 % PROPOSED PAPER STRUCTURE66 67 % Introduction68 % Problem being solved, background, etc.69 % Current state of the art (and problem with it)70 % The `CerCo approach' (tm)71 % Brief Matita overview72 % Map of paper73 74 % CerCo compiler architecture75 % Description of languages76 % Target hardware description77 78 % Compiler proof79 % Structure of proof, and high-level discussion80 % Technical devices: structured traces, labelling, etc.81 % Assembler proof82 % Technical issues in front end (Brian?)83 % Main theorem statement84 85 % FramaC plugin86 % Purpose87 % Description of architecture88 % Case study/worked example (crypto example?)89 90 % Formal development91 % Source code repo link92 % Statistics (number of lines, etc.)93 % Description of remaining axioms --- try and explain them away/make them sound reasonable94 95 % Conclusions96 % Summary97 % Related work98 % Future work99 100 % Bibliography101 102 65 \title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the 103 66 financial 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 4 2 % Summary 5 3 % Related work 6 4 % Future work 5 6 \section{Conclusions} 7 \label{sect.conclusions} 7 8 8 9 In 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 1 6 \section{Formal development} 2 7 \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 1 6 \section{FramaC plugin} 2 7 \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 1 8 \section{Introduction} 2 9 \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 1 8 \section{Compiler proof} 2 9 \label{sect.compiler.proof}
Note: See TracChangeset
for help on using the changeset viewer.