Journées annuelles 2024
22 au 24 mai 2024, LIP6, campus de Jussieu, Paris
Programme préliminaire
Mercredi 22 mai
salle 25-26/105
- 09:00. Accueil café
- 10:00. Cyril Cohen
- 11:00. Marc Mezzarobba
- 12:00. Déjeuner à l'Ardoise
- 14:00. Alaa Ibrahim, Positivity Certificates for Linear recurrences
- 15:00. Alexandre Guillemot
- 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
- 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
- 16:00. Pause café
- 16:30. Atelier : Outils pour les preuves calculatoires en mathématiques
- 19:30. Dîner
Vendredi 24 mai
salle 25-26/105
- 09:00. Laurent Théry, Revisiting the FFT in Coq
-
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
- 12:00. Déjeuner à l'Ardoise
