Journées annuelles 2024
22 au 24 mai 2024, LIP6, campus de Jussieu, Paris
Programme
Mercredi 22 mai
salle 2526/105
 09:00. Accueil café
 10:00. Laurent Théry, Revisiting the FFT in Coq
 10:30. Marc Mezzarobba, Calcul de matrices de Stokes d'équations différentielles linéaires de niveau unique 1
 11:30. Discussions
 12:00. Déjeuner à l'Ardoise
 14:00. Alaa Ibrahim, Positivity Certificates for Linear recurrences
 15:00. Alexandre Guillemot, From validated numerics to certified homotopies
résumé
Using validated numerical methods, interval arithmetic and Taylor models, we propose a certified predictorcorrector loop for tracking zeros of polynomial systems with a parameter. We formulate our results in a computational model with adaptative precision, so that there is no discrepancy between what is presented and what is implemented. We provide a Rust implementation which shows tremendous improvement over existing software for certified path tracking.
 16:00. Pause café
 16:30. Atelier
Jeudi 23 mai
Matinée : salle 2425/405

09:30. Eric Goubault, Guaranteed approximations of arbitrarily quantified reachability problems
résumé
In this work, we will show how to compute inner and outer approximations of the set of vectors in R^n satisfying the general quantified formulas of the form: For all x1, exists x2, for all x3, exists x4, … , forall x2k1, exists x2k, z=f(x1,x2,…,x2k1,x2k) where f is a general, possibly nonlinear, function. This will be based on simple interval arithmetic and as such, is only the first step (« order 0 ») of a series of higherorder approximations. If time permits, we will say a few words about how this extends to inner and outer approximations of general quantifier elimination problems. We will exemplify this method on various control applications, e.g. robust reachability (f is the flow function of some discrete or continuous dynamical system), motion planning, various hyper properties etc.
 10:30. Pause café
 11:00. Fredrik Johansson, Generic rings and numerical computation in FLINT
 12:00. Déjeuner à l'Ardoise
Aprèsmidi : salle 2526/105
 14:00. Jean Kieffer, Évaluation de fonctions thêta en temps quasilinéaire uniforme en toute dimension
 15:00. Harald Helfgott, Calculs rigoureux et l'espoir des preuves formelles: une miscellanée sur des thèmes de Goldbach (faible).
 16:00. Pause café
 16:30. Atelier : Outils pour les preuves calculatoires en mathématiques
 19:00. Dîner
Vendredi 24 mai
salle 2526/105

09:30. Assia Mahboubi, Proof transfer for free, with or without univalence
résumé
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of theorems, when such obvious replacements are typically left implicit on paper. This input represents a significant part of the bureaucratic work plaguing the activity of writing formal proofs. This issue is actually specially acute in the context of formally verified computational mathematics.
In this talk, we propose a novel framework for proof transfer, for proof assistants based on dependent type theory, such as Lean, Coq or Agda. This approach relies on original results in type theory (*), as well as on the design and implementation of an automation device, which puts them at work on concrete problems.
This talk will strive to assume little familiarity from the audience with dependent type theory, explaining in particular all the words in the title, and trying to illustrate how properties of the foundations backing a proof assistant may impact the practice of formalizing mathematics.
This is a joint work with Enzo Crance and Cyril Cohen.
(*) for a knowledgeable audience: we propose a novel formulation of type equivalence, used to generalize SozeauTanterTabareau's univalent parametricity translation.
 10:30. Pause café
 11:00. Florent Bréhard, Rounding Error Analysis of an Orbital Collision Probability Evaluation Algorithm
résumé
We present an error analysis of an algorithm due to Serra et al. (Journal of Guidance Control and Dynamics, 2016) for computing the orbital collision probability in the short term encounter model. The algorithm reduces the numerical computation of the collision probability to that of the sum of a series whose coefficients are produced by a linear recurrence relation, and is specifically designed to avoid cancellation issues in the evaluation of the sum. While its numerical stability was observed experimentally and a truncation error bound was derived, the evaluation error was not studied. Here we give a rigorous bound on the accumulated rounding error when Serra et al.’s algorithm is implemented in floatingpoint arithmetic. For a unit roundoff u and a truncation order N , the bound is of the form (N + A)u + o(u), where o(u) stands for small compared to u, explicitly bounded terms. The constant A explicitly depends on the problem parameters and dominates N in practice. Our analysis is based on the observation that the generating series of the errors affecting each individual term is solution to a perturbed form of a differential equation satisfied by the Laplace transform of a function related to the collision probability. This is a joint work with Denis Arzelier, Mioara Joldes and Marc Mezzarobba.
 12:00. Déjeuner à l'Ardoise