Changeset 1365 for Deliverables/D4.24.3/reports/D43.tex
 Timestamp:
 Oct 13, 2011, 11:30:36 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.24.3/reports/D43.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 backend 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.