Formally Verified Approximations of Definite Integrals

Henessey and Patterson Appendix H has a good section with reference by the same Golberg who wrote the What Every Computer Scientist Should Know About Floating-Point Arithmetic

  • NaN
  • Denormalized numbers

Fixed point smtlib encoding pysmt

john harrison p-adic and floats are similar? msb vs lsb?

harrison book - Proving About Real Numbers Boldo Melquiond book - computer arithemtic and formal proofs

Can I directly write down the principals of interval arithmetic? The contraction map principle. True ODES are the capability to do something for all dt The dangers of fast-math flags. Herbie comments ocaml crlibm

Herbie is super cool.

  1. you can just do rancom sampling to estimate errors, with extreme multiprecision accuracy and regular. Dynamic analysis in a sense?
  2. rewriitng Denali

Arith_2021 - a conference on FP? FPTalks

Hamming book kahan summation

What is fluctuat? precisa precision tuning FPTaylor demo - scaling numerical rounding analysis FPBench , FPTalk Herbie shaman - another error tracking thing

Gappa Sollya textbook on coq floating point FlocQ

Verified plotting -Melquiond generating correctly rounded math libraries for 32 bit Fluctuat analyzer

Textbook Formal Verification fo Floatng Point Hardware

My coq pendulum swing up. Could I verify it? Adaptive Precision Floating-Point Arithmetic and Fast Robust Predicates for Computational Geometry - synethesizing a correctly rounded floating point guy

CRLibm MetaLbim gappa tocatta I guess why3 has extensive support for floating point? a multirpecision library verified using why3 Generating Correctly Rounded Math Libraries for New Floating Point Variants (full) λS: Computable Semantics for Diff’ble Programming with HO Functions and Datatypes (full)