Ignore:
Timestamp:
Dec 8, 2010, 3:14:02 PM (9 years ago)
Author:
mulligan
Message:

Implemented some of the changes suggested by CSC.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r384 r390  
    6262\textbf{
    6363Report n. D4.1\\
    64 Intel 8051/8052 emulator prototype, and formalisation in Matita}
     64Verified Compiler---Back End}
    6565\end{LARGE}
    6666\end{center}
     
    7777\begin{large}
    7878Main Authors:\\
    79 Claudio Sacerdoti Coen and Dominic P. Mulligan
     79Dominic P. Mulligan and Claudio Sacerdoti Coen
    8080\end{large}
    8181\end{center}
     
    503503Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
    504504
     505\subsection{Validation}
     506\label{subsect.matita.validation}
     507
     508The Matita emulator is executable from within Matita (naturally, the speed of execution is only a fraction of the speed of the O'Caml emulator).
     509
     510\subsection{Future work}
     511\label{subsect.future.work}
     512
     513The Matita emulator is written in the latest public Subversion repository version of Matita.
     514However, this version is in an intermediate stage between the `old' Matita, and a new, more streamlined version of the proof assistant.
     515As a result, some key features of the system are currently missing in the repository version of Matita, most notably program code extraction from a Matita theory file.
     516
     517The new, rewritten version of Matita reinstates the missing functionality.
     518We plan, once the newer version is released, to port the Matita emulator to the most up-to-date version of the proof assistant.
     519This will allow us to extract a verified O'Caml emulator from the Matita theory files.
     520
     521\newpage
     522
     523\section{Listing of O'Caml files}
     524\label{sect.listing.ocaml.files}
     525
     526\newpage
     527
     528\section{Listing of Matita files}
     529\label{sect.listing.matita.files}
     530
    505531\end{document}
Note: See TracChangeset for help on using the changeset viewer.