NuSCAP

Journées annuelles 2024

22 au 24 mai 2024, LIP6, campus de Jussieu, Paris

Programme

Mercredi 22 mai

salle 25-26/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 predictor-corrector 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 24-25/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 x2k-1, exists x2k, z=f(x1,x2,…,x2k-1,x2k) where f is a general, possibly non-linear, function. This will be based on simple interval arithmetic and as such, is only the first step (« order 0 ») of a series of higher-order 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ès-midi : salle 25-26/105

• 14:00. Jean Kieffer, Évaluation de fonctions thêta en temps quasi-liné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 25-26/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 Sozeau-Tanter-Tabareau'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 floating-point 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

   

©