Changeset 812
- Timestamp:
- May 16, 2011, 5:43:15 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r811 r812 358 358 To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans. 359 359 In 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.360 From within the bitvector module (top) bitvectors are just lists of bits and no guarantee is provided on sizes. 361 However, the module's interface (bottom) enforces size invariants in the rest of the code. 362 362 363 363 In 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.