Changeset 572


Ignore:
Timestamp:
Feb 18, 2011, 1:28:31 PM (6 years ago)
Author:
mulligan
Message:

tweaked the abstract

File:
1 edited

Legend:

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

    r571 r572  
    6969The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
    7070
    71 The formalisation proceeded in two stages, first implementing an O'Caml prototype for quickly `ironing out' bugs.
    72 We then ported the O'Caml emulator to Matita.
     71The formalisation proceeded in two stages, first implementing an O'Caml prototype, for quickly `ironing out' bugs, and then porting the O'Caml emulator to Matita.
    7372Though mostly straight-forward, this porting presented multiple problems.
    74 Of particular interest is how we handled the non-orthoganality of the MSC-51's instruction set.
     73Of particular interest is how we handled the unorthoganality of the MSC-51's instruction set.
    7574In O'Caml, this was handled with polymorphic variants.
    7675In Matita, we achieved the same effect with a non-standard use of dependent types.
Note: See TracChangeset for help on using the changeset viewer.