Changeset 501


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

more changes

File:
1 edited

Legend:

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

    r495 r501  
    3434\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
    3535\authorrunning{C. Sacerdoti Coen and D. P. Mulligan}
    36 \title{An executable formalisation of the 8051/8052 series microprocessor in Matita}
    37 \titlerunning{An executable formalisation of the 8051/8052}
     36\title{An executable formalisation of the MCS-51 microprocessor in Matita}
     37\titlerunning{An executable formalisation of the MCS-51}
    3838\institute{Dipartimento di Scienze dell'Informazione, University of Bologna}
    3939
     
    5151Of particular interest is how we handle the extreme non-orthoganality of the MSC-51's instruction set.
    5252In O'Caml, this was handled through heavy use of polymorphic variants.
    53 In Matita, we achieve the same effect through a novel use of dependent types.
     53In Matita, we achieve the same effect through a non-standard use of dependent types.
    5454
    5555Both the O'Caml and Matita emulators are `executable'.
Note: See TracChangeset for help on using the changeset viewer.