Changeset 501

Show
Ignore:
Timestamp:
02/11/11 17:35:18 (2 years ago)
Author:
mulligan
Message:

more changes

Files:
1 modified

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'.