source: Deliverables/D4.4/report.tex @ 3180

Last change on this file since 3180 was 3143, checked in by sacerdot, 7 years ago

More papers pulled into the report.

File size: 2.9 KB
Line 
1\documentclass[11pt, epsf, a4wide]{article}
2
3\usepackage{../style/cerco}
4\usepackage{pdfpages}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb} 
9\usepackage[english]{babel}
10\usepackage{graphicx}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14\usepackage{url}
15\usepackage{bbm}
16
17\title{
18INFORMATION AND COMMUNICATION TECHNOLOGIES\\
19(ICT)\\
20PROGRAMME\\
21\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
22
23\lstdefinelanguage{matita-ocaml}
24  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
25   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
26   morekeywords={[3]type,of},
27   mathescape=true,
28  }
29
30\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
31        keywordstyle=\color{red}\bfseries,
32        keywordstyle=[2]\color{blue},
33        keywordstyle=[3]\color{blue}\bfseries,
34        commentstyle=\color{green},
35        stringstyle=\color{blue},
36        showspaces=false,showstringspaces=false}
37
38\lstset{extendedchars=false}
39\lstset{inputencoding=utf8x}
40\DeclareUnicodeCharacter{8797}{:=}
41\DeclareUnicodeCharacter{10746}{++}
42\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
43\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
44
45\date{}
46\author{}
47
48\begin{document}
49
50\thispagestyle{empty}
51
52\vspace*{-1cm}
53\begin{center}
54\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
55\end{center}
56
57\begin{minipage}{\textwidth}
58\maketitle
59\end{minipage}
60
61\vspace*{0.5cm}
62\begin{center}
63\begin{LARGE}
64\textbf{
65Report n. D4.4\\
66Back-end Correctness Proof}
67\end{LARGE} 
68\end{center}
69
70\vspace*{2cm}
71\begin{center}
72\begin{large}
73Version 1.0
74\end{large}
75\end{center}
76
77\vspace*{0.5cm}
78\begin{center}
79\begin{large}
80Main Authors:\\
81XXXX %Dominic P. Mulligan and Claudio Sacerdoti Coen
82\end{large}
83\end{center}
84
85\vspace*{\fill}
86
87\noindent
88Project Acronym: \cerco{}\\
89Project full title: Certified Complexity\\
90Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
91
92\clearpage
93\pagestyle{myheadings}
94\markright{\cerco{}, FP7-ICT-2009-C-243881}
95
96\newpage
97
98\vspace*{7cm}
99\paragraph{Abstract}
100xxx
101
102\newpage
103
104\tableofcontents
105
106\newpage
107
108\section{Task}
109\label{sect.task}
110
111The Grant Agreement describes deliverable D4.4 as follows:
112\begin{quotation}
113\textbf{Back-end correctness proof}: Formally checked proof of the semantics correspondence between the intermediate code and the target code, and of the preservation/modification of the control flow for complexity analysis. An extensive validation of implementation of the Untrusted Cerco Prototype D5.1 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted CerCo Compiler sources and CIC encoding (D2.2, D5.1 and D4.2).
114\end{quotation}
115
116\newpage
117
118\includepdf[pages={-}]{itp2013.pdf}
119\includepdf[pages={-}]{mauro.pdf}
120\includepdf[pages={-}]{cpp-2012-asm.pdf}
121\includepdf[pages={-}]{cpp-2012-policy.pdf}
122
123\end{document}
Note: See TracBrowser for help on using the repository browser.