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

Last change on this file since 3194 was 3194, checked in by tranquil, 7 years ago

more on the role of the stack in the back end pass.
moved mauro.tex as an include of paolo.tex

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={-}]{paolo.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.