Ignore:
Timestamp:
Oct 14, 2011, 3:51:09 PM (8 years ago)
Author:
mulligan
Message:

changes to file based on claudio's suggestions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1366 r1373  
    146146\label{subsect.abstracting.related.languages}
    147147
     148As mentioned in the report for Deliverable D4.2, a systematic process of abstraction, over the O'Caml code, has taken place in the Matita encoding.
     149In particular, we have merged many of the syntaxes of the intermediate languages (i.e. RTL, ERTL, LTL and LIN) into a single `joint' syntax, which is parameterised by various types.
     150Equivalent intermediate languages to those present in the O'Caml code can be recovered by specialising this joint structure.
     151
    148152%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    149153% SECTION.                                                                    %
     
    158162\label{subsect.what.we.do.not.implement}
    159163
     164There are a number of features that are not yet implemented in the semantics, and some routine axioms remaining.
     165We summarise them here:
     166\begin{itemize}
     167\item
     168Like in the
     169\end{itemize}
     170
    160171%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    161172% SECTION.                                                                    %
     
    171182\section{Code listing}
    172183\label{sect.code.listing}
     184
     185%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     186% SECTION.                                                                    %
     187%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     188\subsection{Listing of files}
     189\label{subsect.listing.files}
    173190
    174191Semantics specific files (files relating to language translations ommitted):
     
    178195\hline
    179196\texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
     197\texttt{RTLabs/semantics.ma} & The semantics of RTLabs \\
    180198\texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
     199\texttt{joint/SemanticUtils.ma} & Generic utilities used in the semantics of all `joint' intermediate languages \\
    181200\texttt{RTL/RTL.ma} & The syntax of RTL \\
     201\texttt{RTL/semantics.ma} & The semantics of RTL \\
    182202\texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
     203\texttt{ERTL/semantics.ma} & The semantics of ERTL \\
    183204\texttt{LTL/LTL.ma} & The syntax of LTL \\
     205\texttt{LTL/semantics.ma} & The semantics of LTL \\
    184206\texttt{LIN/LIN.ma} & The syntax of LIN \\
     207\texttt{LIN/semantics.ma} & The semantics of LIN
    185208\end{tabular*}
    186209\end{center}
    187 
    188 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    189 % SECTION.                                                                    %
    190 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    191 \subsection{Listing of files}
    192 \label{subsect.listing.files}
    193210
    194211%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     
    198215\label{subsect.listing.important.functions.axioms}
    199216
     217We list some important functions and axioms in the backend semantics:
     218
    200219\end{document}
Note: See TracChangeset for help on using the changeset viewer.