Changeset 1365 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 13, 2011, 11:30:36 AM (9 years ago)
- Location:
- Deliverables/D4.2-4.3/reports
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1364 r1365 114 114 The Grant Agreement states that Task T4.2, entitled `Functional encoding in the Calculus of Constructions' has associated Deliverable D4.2, consisting of the following: 115 115 \begin{quotation} 116 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.116 CIC encoding: Back-end: Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler. This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2. A first validation of the design principles and implementation choices for the Untrusted Cost-annotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Cost-annotating OCaml Compiler sources. 117 117 \end{quotation} 118 118 This report details our implementation of this deliverable. -
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.