Institut de recherche mathématique avancée
L'institut
À la une
Agenda
-
Jeudi 21 septembre 2023 - 09h00 Séminaire IRMIA++
-
Arthur Charguéraud :
Interactive Program Verification
- Lieu : Salle de conférences IRMA
-
Résumé : Formal Verification enables one to prove that a program does not contain any bug. In this talk, I will present state-of-the-art techniques for formally verifying the implementation of a nontrivial algorithm or data structure. First, I will explain how to formulate as a mathematical theorem a statement of the form: "this program behaves as intended". Second, I will explain how to leverage an "interactive proof assistant", a tool for developing machine-checked mathematical proofs, for reasoning about the behavior of the source code of the program. Finally, I will give a survey of complex programs that have been formally verified in the past decade, assessing the progress made since the pioneering work by Hoare-Floyd-Dijkstra in the late 60's.
The seminar will be also broadcasted via BBB: https://bbb.unistra.fr/b/hum-51d-suf-mzq
Arthur Charguéraud is an Inria researcher, member of the ICube lab since 2016. He completed his PhD in 2010 at Inria Paris-Rocquencourt, then spent 18 months as a post-doc at the Max Plank Institute for Software Systems in Kaiserslautern. He was recruited at Inria Saclay in 2012, then moved to Strasbourg in 2016. His research is focused on program verification and program optimization.
-
Jeudi 21 septembre 2023 - 10h30 Groupe de travail Theorie de Hodge des morphismes et faisceaux pervers
-
Dragos Fratila :
Réunion de préparation
- Lieu : Salle de séminaires IRMA
-
Jeudi 21 septembre 2023 - 14h00 Séminaire Arithmétique et géométrie algébrique
-
Emanuele Macri :
Vector bundles on Fano threefolds
- Lieu : Salle de séminaires IRMA
-
Résumé : A celebrated part in the classification of Fano threefold is Mukai's vector bundle method. One of the main result is an existence (and rigidity) result for vector bundles with rank dividing the genus, for prime Fano threefolds of index 1. Unfortunately, in the literature, the proof has a gap. I will present joint work with Arend Bayer and Alexander Kuznetsov, where we fill this gap.
-
Jeudi 21 septembre 2023 - 16h30 Séminaire Doctorants
-
Alex Podgorny :
Analogie entre TCL et TVE
- Lieu : Salle de conférences IRMA
-
Résumé : L'échantillon de n variables aléatoires réelles indépendantes et identiquement distribuées est l'objet d'étude le plus basique des statistiques. Le comportement de la somme d'un tel échantillon (sous l'hypothèse d'une variance finie) est bien connu : c'est le Théorème Central Limite (TCL). Comme son nom l'indique, ce théorème nous renseigne sur la partie "centrale" de la distribution (là où le poids de probabilité est concentré). Si au contraire nous voulons nous intéresser à la queue droite (resp. gauche) de la distribution, la variable d'intérêt sera le maximum (resp. le minimum) de l'échantillon. À l'instar de la somme, le comportement du maximum est aussi connu : c'est le Théorème des Valeurs Extrêmes (TVE). L'objectif de ce séminaire est d'explorer l'analogie entre ces deux théorèmes fondamentaux.
-
Vendredi 22 septembre 2023 - 16h00 Colloquium Mathématique
-
Emanuele Macri :
Hyper-Kähler manifolds and Lagrangian fibrations
- Lieu : Salle de conférences IRMA
-
Résumé : A hyper-Kähler manifold is a complex Kähler manifold that is simply connected, compact, and has a unique holomorphic symplectic form, up to constants.
This important class of manifolds has been studied in the past in many contexts, from an arithmetic, algebraic, geometric point of view, and in applications to physics and dynamics.
The theory in dimension two, namely K3 surfaces, is well understood.
The aim of the seminar is to give an introduction to the theory of hyper-Kähler manifolds in higher dimension, from a point of view of their classification; in particular, about existence of Lagrangian fibrations.
We will present some results in dimension four, obtained in collaboration with Olivier Debarre, Daniel Huybrechts and Claire Voisin.
-
Lundi 25 septembre 2023 - 14h00 Séminaire GT3
-
Simon Allais :
Ordonnabilité et sélecteurs spectraux
- Lieu : Salle de séminaires IRMA
-
Résumé : En 2000, Eliashberg et Polterovich introduisirent la notion d'ordonnabilité pour étudier la structure des groupes de contactomorphismes et des classes d'isotopie de sous-variétés legendriennes. En peu de mots, le groupe des contactomorphismes est ordonnable si la relation binaire sur les flots de contact au temps 1 naturellement induite par l'ordre partiel sur leurs hamiltoniens est elle-même un ordre partiel. Au cours des deux dernières décennies, ordonnabilité et non-ordonnabilité ont été principalement étudiées au moyen de selecteurs spectraux basés sur des théories dérivées de celle de Floer et sur les fonctions génératrices. Dans cet exposé, nous expliquerons en quoi l'ordonnabilité est équivalente à l'existence de sélecteurs spectraux et en donnerons quelques applications.