Title: Foundational end-to-end verification of numerical programs
Author: Andrew Appel

Abstract:
Program verification is foundational when it assumes only the axioms
of logic, the specification of the machine to be run on, and the
specification of desired input/output behavior. It is end-to-end when
the machine model is low-level, the desired specification is
high-level, and all the component verifications compose together into
a single machine-checked theorem. Foundational E2E verification has
been demonstrated in a few application domains (cryptography,
operating systems, compilers). Now it's time to apply it to scientific
computing. This requires several different kinds of proofs:
correctness of a low-level program w.r.t. a floating-point functional
model, data structure proofs, floating-point round-off error analysis,
method-error bounds, convergence proofs. Each kind of proof needs its
own tools and libraries, and its own experts. Fortunately, the proof
assistants for a logical framework provides a structure in which all
these tools and libraries can connect, and these experts can
collaborate.