|
Finite
Machine
Word
Library
Title: |
Finite Machine Word Library |
Authors:
|
Joel Beeren,
Matthew Fernandez,
Xin Gao,
Gerwin Klein,
Rafal Kolanski,
Japheth Lim,
Corey Lewis,
Daniel Matichuk and
Thomas Sewell
|
Submission date: |
2016-06-09 |
Abstract: |
This entry contains an extension to the Isabelle library for
fixed-width machine words. In particular, the entry adds quickcheck setup
for words, printing as hexadecimals, additional operations, reasoning
about alignment, signed words, enumerations of words, normalisation of
word numerals, and an extensive library of properties about generic
fixed-width words, as well as an instantiation of many of these to the
commonly used 32 and 64-bit bases. |
BibTeX: |
@article{Word_Lib-AFP,
author = {Joel Beeren and Matthew Fernandez and Xin Gao and Gerwin Klein and Rafal Kolanski and Japheth Lim and Corey Lewis and Daniel Matichuk and Thomas Sewell},
title = {Finite Machine Word Library},
journal = {Archive of Formal Proofs},
month = jun,
year = 2016,
note = {\url{http://isa-afp.org/entries/Word_Lib.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Used by: |
CakeML, Complx, IEEE_Floating_Point, IP_Addresses |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|