Changeset 1365 for Deliverables/D4.2-4.3


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

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  
    114114The Grant Agreement states that Task T4.2, entitled `Functional encoding in the Calculus of Constructions' has associated Deliverable D4.2, consisting of the following:
    115115\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.
     116CIC 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.
    117117\end{quotation}
    118118This report details our implementation of this deliverable.

  • 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.