fixed-point arithmetic
floating-point arithmetic
theorem-proving
HOL