A Parameterized Floating-Point Formalizaton in HOL Light.

Charles Jacobsen Alexey Solovyev Ganesh Gopalakrishnan

Published in: Electron. Notes Theor. Comput. Sci. (2015)

Keyphrases

floating point
fixed point
square root
sparse matrices
theorem prover
formal methods
instruction set
natural deduction
floating point arithmetic
computer vision
interval arithmetic
fast fourier transform
hardware and software
constraint satisfaction problems
post processing
software engineering
data structure