A Formal Model for the Floating Point Computations for the Dependently-Typed Lambda Calculus

S. V. Antonov, Student, e-mail: antonovsergey93@gmail.com, M. A. Krivchikov, Researcher, e-mail: maxim.krivchikov@gmail.com, Faculty of Mechanics and Mathematics and Institute of Mechanics, Lomonosov Moscow State University, Moscow, Russia

The proof of correctness for the computational methods which are used in the complex physical simulation software is an important part of the formal verification process for such a software. The high-performance physical simulation algorithms are usually implemented by the means of floating point computing model based on IEEE 754 Standard.

In this paper a new formal model for IEEE 754 floating point numbers and arithmetic operations is presented. The model is implemented in Coq proof assistant. The arithmetic operations are executable so that it is possible to obtain the results of computation in Coq. The model is abstract enough to be expressed in any dependently-typed lambda calculi with support for the dependent sums, finite types with two and three elements and the natural numbers. The model is tested by comparison of the computation results for model and for hardware floating point implementations using the fragment of code from production physical simulation package.

The floating-point computations model includes the abstract interface for the arithmetic operations on some approximation of real numbers. Based on such interface, the authors specify a simple language of arithmetic expressions with replaceable implementations of arithmetic. By means of the language, the error which is introduced in the mentioned code fragment by replacing exact real number operations with inexact floating point equivalents is justified.

Keywords: formal models, formal verification, lambda-calculus, programming with dependent types, floating point numbers, floating point inaccuracy, formal semantics

pp. 25–31