3 ms·
The Little Prover might be a good choice: it’s about ACL2, which was used to prove various floating point implementations were correct. It’s a fairly accessible
by fiddlerwoaroof 6y ago
The Little Prover might be a good choice: it’s about ACL2, which was used to prove various floating point implementations were correct. It’s a fairly accessible guide to proving theorems in this system.