Changeset 494


Ignore:
Timestamp:
Feb 11, 2011, 12:11:12 PM (6 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

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

    r493 r494  
    66\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
    77\authorrunning{C. Sacerdoti Coen and D. P. Mulligan}
    8 \title{An executable model of the 8051/8052 series microprocessor in Matita}
    9 \titlerunning{An executable model of the 8051/8052}
     8\title{An executable formalisation of the 8051/8052 series microprocessor in Matita}
     9\titlerunning{An executable formalisation of the 8051/8052}
    1010\institute{Dipartimento di Scienze dell'Informazione, University of Bologna}
    1111
     
    118118\label{subsect.overview.paper}
    119119
     120In Section~\ref{sect.development.strategy} we provide a brief overview of how we designed and implemented the formalised microprocessor emulator.
     121In Section~\ref{sect.design.issues.formalisation} we describe how we made use of dependent types to handle some of the idiosyncracies of the microprocessor.
     122In Section~\ref{sect.related.work} we describe the relation our work has to
     123
    120124%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    121125% SECTION                                                                      %
     
    127131% SECTION                                                                      %
    128132%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    129 \section{Putting dependent types to work}
    130 \label{sect.putting.dependent.types.to.work}
     133\section{Design issues in the formalisation}
     134\label{sect.design.issues.formalisation}
     135
     136%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     137% SECTION                                                                      %
     138%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     139\subsection{Labels and pseudoinstructions}
     140\label{subsect.labels.pseudoinstructions}
     141
     142%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     143% SECTION                                                                      %
     144%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     145\subsection{Putting dependent types to work}
     146\label{subsect.putting.dependent.types.to.work}
     147
     148%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     149% SECTION                                                                      %
     150%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     151\section{Validation}
     152\label{sect.validation}
    131153
    132154%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.