Index: Deliverables/D4.1/ITPPaper/itp2011.tex
===================================================================
 Deliverables/D4.1/ITPPaper/itp2011.tex (revision 526)
+++ Deliverables/D4.1/ITPPaper/itp2011.tex (revision 527)
@@ 32,5 +32,5 @@
{keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on},
morekeywords={[2]whd,normalize,elim,cases,destruct},
 morekeywords={[3]type,ofm},
+ morekeywords={[3]type,of,val},
mathescape=true,
}
@@ 49,6 +49,7 @@
\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
\authorrunning{C. Sacerdoti Coen and D. P. Mulligan}
+% Who is first author? Is CSC classed as a `S', or as a `C'?
+\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
+\authorrunning{D. P. Mulligan and C. Sacerdoti Coen}
\title{An executable formalisation of the MCS51 microprocessor in Matita}
\titlerunning{An executable formalisation of the MCS51}
@@ 218,6 +219,11 @@
% SECTION %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{From O'Caml prototype to Matita formalisation}
\label{sect.from.o'caml.prototype.matita.formalisation}
+\section{Design issues in the formalisation}
+\label{sect.design.issues.formalisation}
+
+From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.
+
+\subsection{Development strategy}
+\label{subsect.development.strategy}
Our implementation progressed in two stages:
@@ 238,14 +244,32 @@
% SECTION %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Design issues in the formalisation}
\label{sect.design.issues.formalisation}

From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SECTION %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Representation of integers}
\label{subsect.representation.integers}
+
+Integers are represented using bitvectors, i.e. fixed length vectors of booleans.
+In our O'Caml emulator, we `faked' bitvectors using phantom types and polymorphic variants, like so:
+\begin{lstlisting}
+type bit = bool
+type 'a vect = bit list
+type word = [`Sixteen] vect
+type byte = [`Eight] vect
+\end{lstlisting}
+Using this technique, we can provide precise typings for utility and arithmetic functions giving us some stronger guarantees of type safety.
+For instance, functions that split \texttt{word}s into their constituent \texttt{byte}s:
+\begin{lstlisting}
+val from_word: word > byte * byte
+\end{lstlisting}
+In Matita, we are able to use the full power of dependent types to define `real' bitvectors:
+\begin{lstlisting}
+inductive Vector (A: Type[0]): nat → Type[0] ≝
+ VEmpty: Vector A O
+ VCons: ∀n: nat. A → Vector A n → Vector A (S n).
+\end{lstlisting}
+We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
+We may use Matita's type system to provide even stronger guarantees, here on a function that splits a vector into two pieces at any index, providing that the index is smaller than the length of the \texttt{Vector} to be split:
+\begin{lstlisting}
+let rec split (A: Type[0]) (m,n: nat) on m:
+ Vector A (plus m n) $\rightarrow$ (Vector A m) $\times$ (Vector A n) := ...
+\end{lstlisting}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%