3 papers
cs.PL2022
Dandelion: Certified Approximations of Elementary Functions
Heiko Becker, Mohit Tekriwal, Eva Darulova +2
Elementary function operations such as sin and exp cannot in general be computed exactly on today's digital computers, and thus have to be approximated. The standard approximations…
cs.PL2021
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran +2
Proof engineering efforts using interactive theorem proving have yielded several impressive projects in software systems and mathematics. A key obstacle to such efforts is the requ…
cs.PL2018
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Pancheckha, Eva Darulova +1
Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, ea…