A Monte Carlo Method for High Dimensional Integration.
Analytické derivovanie na číslicovom počítači
Axiomatisation des manipulations symboliques en calcul des prédicats
Fast and correctly rounded logarithms in double-precision
This article is a case study in the implementation of a portable, proven and efficient correctly rounded elementary function in double-precision. We describe the methodology used to achieve these goals in the crlibm library. There are two novel aspects to this approach. The first is the proof framework, and in general the techniques used to balance performance and provability. The second is the introduction of processor-specific optimization to get performance equivalent to the best current...
One method for proving inequalities by computer.