Butler, R. W. Formalization of the Integral Calculus in the PVS Theorem Prover. JFR 2009, 2, 1-26.