Ignore:
Timestamp:
Feb 17, 2011, 2:52:34 PM (9 years ago)
Author:
mulligan
Message:

Emulator fixed for Wilmer

Location:
Deliverables/D4.1/ITP-Paper
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.bib

    r555 r557  
    125125
    126126@misc
     127{ cerco-report:2011,
     128  title = {D4.1: executable formal semantics of machine code},
     129  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}},
     130  year = {2011},
     131  key = {{CerCo-report}}
     132}
     133
     134@misc
    127135{ mcu8051ide:2010,
    128136  title = {{MCU 8051 IDE} 1.3.11},
     
    151159@misc
    152160{ siemens:2011,
    153   title = {Siemens Semiconductor Group 8051 derivative instruction set},
     161  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
    154162  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
    155163  year = {2011},
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r556 r557  
    222222In Section~\ref{sect.conclusions} we conclude the paper.
    223223
    224 In Appendices~\ref{sect.listing.main.ocaml.functions} and~\ref{sect.listing.main.matita.functions} we provide a brief overview of the main functions in our implementation, and describe at a high level what they do.
    225 
    226224%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    227225% SECTION                                                                      %
     
    233231Matita's syntax is largely straightforward to those familiar with Coq or O'Caml.
    234232The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically.
     233
     234A full account of the formalisation can be found in~\cite{cerco-report:2011}.
    235235
    236236\subsection{Development strategy}
     
    282282The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits).
    283283To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
    284 In our O'Caml emulator, we `faked' bitvectors using phantom types implemented with polymorphic variants\cite{phantom_types_ocaml}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
     284In our O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
    285285From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
    286286However, the module's interface (right column) enforces the size invariants in the rest of the code.
     
    734734\bibliography{itp-2011.bib}
    735735
     736\end{document}
     737
    736738\newpage
    737739
Note: See TracChangeset for help on using the changeset viewer.