Room 206 (2nd floor, badged access)
5 November 2026 - 14h00
Fast and reliable exact real computations through functional programming.
by Yann Kieffer from LCIS and Verimag
invited by Sylvain BOULME
5 November 2026 - 14h00
Fast and reliable exact real computations through functional programming.
by Yann Kieffer from LCIS and Verimag
invited by Sylvain BOULME
Abstract: We present yet another attempt at exact computation with real numbers. Our objectives are asymptotic optimality of computational complexity, as well as the provability of the code. We use an oracle model of real numbers, encoded as functions in the Haskell programming language: such a function takes a precision as its only argument, and answers with an approximation of the real number it represents, up to that precision. We will explain how usual operations and functions on the reals are encoded, the relationship with constructive mathematics, the constraints and difficulties that come our way, the perspectives for the implementation of unstable numerical algorithms, and the next step of the project - namely, proofs.
This work is the basis for a 6-months stay at Verimag, during which I aim at proving these programs using the Rocq proof assistant.
