NuSCAP

Journées annuelles 2025

25 au 27 juin 2025, LS2N, Nantes

La rencontre se déroulera dans le bâtiment 34, situé 2, Chemin de la Houssinière à Nantes.

Orateurs : Xavier Allamigeon (Tropical, Inria Saclay, CMAP, École Polytechnique), Alexandre Goldsztejn (CNRS-LS2N, Nantes), Stef Graillat (LIP6, Sorbonne Université), Olivier Hénot (CMAP, École Polytechnique), Tom Hubrecht (Pascaline, LIP, ENS Lyon), Mioara Joldes (CNRS-LAAS, Toulouse), Guillaume Melquiond (Toccata, Inria Saclay), Arnaud Minondo (MAX, LIX, École Polytechnique), Josué Moreau (Toccata, Inria Saclay), Bruno Salvy (Pascaline, Inria Lyon, LIP, ENS Lyon).

Programme

Mercredi 25 juin

salle

• 09:00. Accueil café
• 10:00. Mioara Joldes (CNRS-LAAS, Toulouse),
  résumé

• 11:00. Guillaume Melquiond (Toccata, Inria Saclay), Floating-point error analysis using CoqInterval
  résumé

  CoqInterval is a set of strategies for the Rocq proof assistant to help reasoning about inequalities of real-valued expressions. It was originally designed to automatically prove error bounds on method errors. To do so, it can compute reliable polynomial approximations using Taylor models, among other things. But lately, it has gained the ability to reason about rounding errors too. During this talk, I will show how the library can be used to formally verify the correctness of fixed- and floating-point code, and how it differs from related tools like Gappa.

• 12:00. Déjeuner
• 14:00. Josué Moreau (Toccata, Inria Saclay), A safe low-level language for computer algebra and its formally verified compiler
  résumé

  I will present Capla, a programming language for writing low-level libraries for computer algebra systems. Such libraries (GMP, BLAS/LAPACK, etc) are usually written in C, Fortran, and Assembly, and make heavy use of arrays and pointers. The proposed language is halfway between C and Rust with a type system similar to the one of SPARK. It does not have any undefined behavior and is designed to ease the deductive verification of programs, while being low-level enough to be suitable for this kind of computationally intensive applications. I have also implemented a compiler for this language, based on the CompCert compiler. The safety of the language has been formally proved using the Rocq proof assistant, and so has the property of semantics preservation for the compiler.

• 15:00. Olivier Hénot (CMAP, École Polytechnique),
  résumé

• 16:00. Pause café
• 16:30. Atelier

Jeudi 26 juin

Matinée : salle

• 09:30. Alexandre Goldsztejn (CNRS-LS2N, Nantes),
  résumé

• 10:30. Pause café
• 11:00. Xavier Allamigeon (Tropical, Inria Saclay, CMAP, École Polytechnique),
  résumé

• 12:00. Déjeuner

Après-midi : salle

• 14:00. Bruno Salvy (Pascaline, Inria Lyon, LIP, ENS Lyon), Positivity Proofs for Linear Recurrences through Contracted Cones
  résumé

  Deciding the positivity of a sequence defined by a linear recurrence with polynomial coefficients and initial conditions is difficult in general. Even in the case of recurrences with constant coefficients, it is known to be decidable only for order up to 5. We consider a large class of linear recurrences of arbitrary order, with polynomial coefficients, for which an algorithm decides positivity for initial conditions outside of a hyperplane. The underlying algorithm constructs a cone, contracted by the recurrence operator, that allows a proof of positivity by induction. The existence and construction of such cones relies on the extension of the classical Perron-Frobenius theory to matrices leaving a cone invariant.

  This is joint work with Alaa Ibrahim

• 15:00. Tom Hubrecht (Pascaline, LIP, ENS Lyon), .
  résumé

• 16:00. Pause café
• 16:30. Atelier :
• 19:00. Dîner

Vendredi 27 juin

salle

• 10:00. Stef Graillat (LIP6, Sorbonne Université), Condense and Distill: fast distillation of large floating-point sums via condensation
  résumé

  Floating-point summation is a fundamental task at the heart of many scientific computing applications. When the sum is very ill conditioned, computing it accurately can become challenging. One can employ distillation methods, which consist in transforming an ill-conditioned sum into an equivalent but well-conditioned one. However, distillation is a very expensive process. In this talk, we propose Condense and Distill, a new distillation method that relies on a preprocessing step that we call condensation, because it transforms the original sum into a far smaller sum, which can then be distilled inexpensively. This condensation step exploits a new, key observation that floating-point addition is exact when the addends have both the same exponent and the same least significant bit. Condense and Distill thus requires accessing the exponent field of the summands. Compared with state-of-the-art summation methods with the same requirement such as the Demmel--Hida method [J. Demmel and Y. Hida, SIAM J. Sci. Comput., 25 (2003), pp. 1214--1248], Condense and Distill presents the significant benefit of running entirely in the working precision, with no need for extra precision. At the same time, it preserves the main advantages of the Demmel--Hida method compared with other methods, in particular those based on error-free transformations such as AccSum [S. M. Rump, T. Ogita, and S. Oishi, SIAM J. Sci. Comput., 31 (2008), pp. 189--224]: namely, its cost is independent of the conditioning, and it exhibits near perfect parallel scaling. We present numerical experiments that confirm that Condense and Distill can reliably and efficiently distill large ill-conditioned sums and performs favorably compared with other state-of-the-art summation methods.

  This is a joint work with Théo Mary.

• 10:30. Pause café
• 11:00. Arnaud Minondo (MAX, LIX, École Polytechnique),
  résumé

• 12:00. Déjeuner