Changeset 812


Ignore:
Timestamp:
May 16, 2011, 5:43:15 PM (9 years ago)
Author:
mulligan
Message:

small change

File:
1 edited

Legend:

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

    r811 r812  
    358358To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans.
    359359In the 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}.
    360 From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
    361 However, the module's interface (right column) enforces size invariants in the rest of the code.
     360From within the bitvector module (top) bitvectors are just lists of bits and no guarantee is provided on sizes.
     361However, the module's interface (bottom) enforces size invariants in the rest of the code.
    362362
    363363In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
Note: See TracChangeset for help on using the changeset viewer.