Ignore:
Timestamp:
Oct 13, 2011, 11:30:36 AM (9 years ago)
Author:
mulligan
Message:

changed description of task in 4.2 report.

added outline and description of task to 4.3 report

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1356 r1365  
    103103
    104104\newpage
     105
     106%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     107% SECTION.                                                                    %
     108%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     109\section{Task}
     110\label{sect.task}
     111
     112The 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}
     114Executable 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}
     116This 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
     162Semantics specific files (files relating to language translations ommitted):
     163\begin{center}
     164\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     165Title & 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
    105188\end{document}
Note: See TracChangeset for help on using the changeset viewer.