Changeset 1365 for Deliverables/D4.2-4.3/reports/D4-3.tex
- Timestamp:
- Oct 13, 2011, 11:30:36 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1356 r1365 103 103 104 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 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 125 % SECTION. % 126 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 127 \section{The backend intermediate languages' semantics in Matita} 128 \label{sect.backend.intermediate.languages.semantics.matita} 129 130 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 131 % SECTION. % 132 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 133 \subsection{Abstracting related languages} 134 \label{subsect.abstracting.related.languages} 135 136 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 137 % SECTION. % 138 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 139 \subsection{Use of dependent types} 140 \label{subsect.use.of.dependent.types} 141 142 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 143 % SECTION. % 144 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 145 \subsection{What we do not implement} 146 \label{subsect.what.we.do.not.implement} 147 148 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 149 % SECTION. % 150 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 151 \section{Future work} 152 \label{sect.future.work} 153 154 \newpage 155 156 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 157 % SECTION. % 158 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 159 \section{Code listing} 160 \label{sect.code.listing} 161 162 Semantics specific files (files relating to language translations ommitted): 163 \begin{center} 164 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 165 Title & Description \\ 166 \hline 167 \texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\ 168 \texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\ 169 \texttt{RTL/RTL.ma} & The syntax of RTL \\ 170 \texttt{ERTL/ERTL.ma} & The syntax of ERTL \\ 171 \texttt{LTL/LTL.ma} & The syntax of LTL \\ 172 \texttt{LIN/LIN.ma} & The syntax of LIN \\ 173 \end{tabular*} 174 \end{center} 175 176 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 177 % SECTION. % 178 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 179 \subsection{Listing of files} 180 \label{subsect.listing.files} 181 182 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 183 % SECTION. % 184 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 185 \subsection{Listing of important functions and axioms} 186 \label{subsect.listing.important.functions.axioms} 187 105 188 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.