1 | \documentclass[11pt, epsf, a4wide]{article} |
---|
2 | |
---|
3 | \usepackage{../../style/cerco} |
---|
4 | |
---|
5 | \usepackage{amsfonts} |
---|
6 | \usepackage{amsmath} |
---|
7 | \usepackage{amssymb} |
---|
8 | \usepackage[english]{babel} |
---|
9 | \usepackage{graphicx} |
---|
10 | \usepackage[utf8x]{inputenc} |
---|
11 | \usepackage{listings} |
---|
12 | \usepackage{stmaryrd} |
---|
13 | \usepackage{url} |
---|
14 | |
---|
15 | \title{ |
---|
16 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
17 | (ICT)\\ |
---|
18 | PROGRAMME\\ |
---|
19 | \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}} |
---|
20 | |
---|
21 | \lstdefinelanguage{matita-ocaml} |
---|
22 | {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try}, |
---|
23 | morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct}, |
---|
24 | morekeywords={[3]type,of}, |
---|
25 | mathescape=true, |
---|
26 | } |
---|
27 | |
---|
28 | \lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false, |
---|
29 | keywordstyle=\color{red}\bfseries, |
---|
30 | keywordstyle=[2]\color{blue}, |
---|
31 | keywordstyle=[3]\color{blue}\bfseries, |
---|
32 | commentstyle=\color{green}, |
---|
33 | stringstyle=\color{blue}, |
---|
34 | showspaces=false,showstringspaces=false} |
---|
35 | |
---|
36 | \lstset{extendedchars=false} |
---|
37 | \lstset{inputencoding=utf8x} |
---|
38 | \DeclareUnicodeCharacter{8797}{:=} |
---|
39 | \DeclareUnicodeCharacter{10746}{++} |
---|
40 | \DeclareUnicodeCharacter{9001}{\ensuremath{\langle}} |
---|
41 | \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} |
---|
42 | |
---|
43 | \date{} |
---|
44 | \author{} |
---|
45 | |
---|
46 | \begin{document} |
---|
47 | |
---|
48 | \thispagestyle{empty} |
---|
49 | |
---|
50 | \vspace*{-1cm} |
---|
51 | \begin{center} |
---|
52 | \includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png} |
---|
53 | \end{center} |
---|
54 | |
---|
55 | \begin{minipage}{\textwidth} |
---|
56 | \maketitle |
---|
57 | \end{minipage} |
---|
58 | |
---|
59 | \vspace*{0.5cm} |
---|
60 | \begin{center} |
---|
61 | \begin{LARGE} |
---|
62 | \textbf{ |
---|
63 | Report n. D4.3\\ |
---|
64 | Formal semantics of intermediate languages |
---|
65 | } |
---|
66 | \end{LARGE} |
---|
67 | \end{center} |
---|
68 | |
---|
69 | \vspace*{2cm} |
---|
70 | \begin{center} |
---|
71 | \begin{large} |
---|
72 | Version 1.0 |
---|
73 | \end{large} |
---|
74 | \end{center} |
---|
75 | |
---|
76 | \vspace*{0.5cm} |
---|
77 | \begin{center} |
---|
78 | \begin{large} |
---|
79 | Main Authors:\\ |
---|
80 | Dominic P. Mulligan and Claudio Sacerdoti Coen |
---|
81 | \end{large} |
---|
82 | \end{center} |
---|
83 | |
---|
84 | \vspace*{\fill} |
---|
85 | |
---|
86 | \noindent |
---|
87 | Project Acronym: \cerco{}\\ |
---|
88 | Project full title: Certified Complexity\\ |
---|
89 | Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ |
---|
90 | |
---|
91 | \clearpage |
---|
92 | \pagestyle{myheadings} |
---|
93 | \markright{\cerco{}, FP7-ICT-2009-C-243881} |
---|
94 | |
---|
95 | \newpage |
---|
96 | |
---|
97 | \vspace*{7cm} |
---|
98 | \paragraph{Abstract} |
---|
99 | |
---|
100 | \newpage |
---|
101 | |
---|
102 | \tableofcontents |
---|
103 | |
---|
104 | \newpage |
---|
105 | |
---|
106 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
107 | % SECTION. % |
---|
108 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
109 | \section{Task} |
---|
110 | \label{sect.task} |
---|
111 | |
---|
112 | The Grant Agreement states that Task T4.3, entitled `Formal semantics of intermediate languages' has associated Deliverable D4.3, consisting of the following: |
---|
113 | \begin{quotation} |
---|
114 | Executable Formal Semantics of back-end intermediate languages: This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it. |
---|
115 | \end{quotation} |
---|
116 | This report details our implementation of this deliverable. |
---|
117 | |
---|
118 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
119 | % SECTION. % |
---|
120 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
121 | \subsection{Connections with other deliverables} |
---|
122 | \label{subsect.connections.with.other.deliverables} |
---|
123 | |
---|
124 | Deliverable D4.3 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4. |
---|
125 | |
---|
126 | Deliverable D2.2, the O'Caml implementation of a cost preserving compiler for a large subset of the C programming language, is the basis upon which we have implemented the current deliverable. |
---|
127 | In particular, the architecture of the compiler, its intermediate languages and their semantics, and the overall implementation of the Matita encodings has been taken from the O'Caml compiler. |
---|
128 | Any variations from the O'Caml design are due to bugs identified in the prototype compiler during the Matita implementation, our identification of code that can be abstracted and made generic, or our use of Matita's much stronger type system to enforce invariants through the use of dependent types. |
---|
129 | |
---|
130 | Deliverable D4.2 can be seen as a `sister' deliverable to the deliverable reported on herein. |
---|
131 | In particular, where this deliverable reports on the encoding in the Calculus of Constructions of the backend semantics, D4.2 is the encoding in the Calculus of Constructions of the mutual translations of those languages. |
---|
132 | As a result, a substantial amount of Matita code is shared between the two deliverables. |
---|
133 | |
---|
134 | Deliverable D4.4, the backend correctness proofs, is the immediate successor of this deliverable. |
---|
135 | |
---|
136 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
137 | % SECTION. % |
---|
138 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
139 | \section{The backend intermediate languages' semantics in Matita} |
---|
140 | \label{sect.backend.intermediate.languages.semantics.matita} |
---|
141 | |
---|
142 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
143 | % SECTION. % |
---|
144 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
145 | \subsection{Abstracting related languages} |
---|
146 | \label{subsect.abstracting.related.languages} |
---|
147 | |
---|
148 | As mentioned in the report for Deliverable D4.2, a systematic process of abstraction, over the O'Caml code, has taken place in the Matita encoding. |
---|
149 | In particular, we have merged many of the syntaxes of the intermediate languages (i.e. RTL, ERTL, LTL and LIN) into a single `joint' syntax, which is parameterised by various types. |
---|
150 | Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure. |
---|
151 | |
---|
152 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
153 | % SECTION. % |
---|
154 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
155 | \subsection{Use of dependent types} |
---|
156 | \label{subsect.use.of.dependent.types} |
---|
157 | |
---|
158 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
159 | % SECTION. % |
---|
160 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
161 | \subsection{What we do not implement} |
---|
162 | \label{subsect.what.we.do.not.implement} |
---|
163 | |
---|
164 | There are a number of features that are not yet implemented in the semantics, and some routine axioms remaining. |
---|
165 | We summarise them here: |
---|
166 | \begin{itemize} |
---|
167 | \item |
---|
168 | Like in the |
---|
169 | \end{itemize} |
---|
170 | |
---|
171 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
172 | % SECTION. % |
---|
173 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
174 | \section{Future work} |
---|
175 | \label{sect.future.work} |
---|
176 | |
---|
177 | \newpage |
---|
178 | |
---|
179 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
180 | % SECTION. % |
---|
181 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
182 | \section{Code listing} |
---|
183 | \label{sect.code.listing} |
---|
184 | |
---|
185 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
186 | % SECTION. % |
---|
187 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
188 | \subsection{Listing of files} |
---|
189 | \label{subsect.listing.files} |
---|
190 | |
---|
191 | Semantics specific files (files relating to language translations ommitted): |
---|
192 | \begin{center} |
---|
193 | \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} |
---|
194 | Title & Description \\ |
---|
195 | \hline |
---|
196 | \texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\ |
---|
197 | \texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\ |
---|
198 | \texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\ |
---|
199 | \texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\ |
---|
200 | \texttt{RTL/RTL.ma} & The syntax of RTL \\ |
---|
201 | \texttt{RTL/semantics.ma} & The semantics of RTL \\ |
---|
202 | \texttt{ERTL/ERTL.ma} & The syntax of ERTL \\ |
---|
203 | \texttt{ERTL/semantics.ma} & The semantics of ERTL \\ |
---|
204 | \texttt{LTL/LTL.ma} & The syntax of LTL \\ |
---|
205 | \texttt{LTL/semantics.ma} & The semantics of LTL \\ |
---|
206 | \texttt{LIN/LIN.ma} & The syntax of LIN \\ |
---|
207 | \texttt{LIN/semantics.ma} & The semantics of LIN |
---|
208 | \end{tabular*} |
---|
209 | \end{center} |
---|
210 | |
---|
211 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
212 | % SECTION. % |
---|
213 | %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% |
---|
214 | \subsection{Listing of important functions and axioms} |
---|
215 | \label{subsect.listing.important.functions.axioms} |
---|
216 | |
---|
217 | We list some important functions and axioms in the backend semantics: |
---|
218 | |
---|
219 | \end{document} |
---|