Synthetic computability can be traced back to Hyland's work on the Effective topos: in this structure, every function is computable, and as such the computability theory can be considered as an internal theory. This also gives an interpretation of oracles for computability as subtoposes of the effective topos. As synthetic computability is based on topos notions, it is also well suited to type theoretic formalism, which will be our framework. In parallel, Homotopy Type Theory (HoTT) emerged to give a type theoretical notion of synthetic homotopy theory. Inside this theory, the notion of space up to path equivalence is primitive (in opposition to set theory, where sets are the primitive notion). A lot of work has been done in recent years to developp this theory, which leads to the work this talk is based on: a paper by Andrew W. Swan describing an adaptation of synthetic computability in HoTT, and the interpretation of oracles as higher modalities. We will see how these notions arise and how they can be generalized to higher types.
Termination is an important property of algorithms, ensuring that they will not run indefinitely. This property is often essential for correctness, yet proving termination can be challenging.
Under the SAPPORO project, we developed an automated technique called Subgraph Counting to prove termination for algorithms modeled as injective double-pushout (DPO) graph rewriting systems. DPO graph rewriting systems model data as graphs and algorithms as sets of rules representing operations that algorithms can perform. Each rule specifies conditions for replacing a subgraph with another.
In this presentation, we focus on the termination of algorithms representable as a single rule. The Subgraph Counting technique relies on the principle that if the number of occurrences of a specific subgraph strictly decreases with each rewriting step, then the rewriting rule will eventually terminates. The key challenge is to estimate the number of occurrences of the subgraph in the graph before and after a rewriting step in an implicit context. We are going to present a sufficient condition on the rewriting rule that makes this estimation possible.
Cette thèse porte sur la stabilisation de problèmes de transmission d’interface impliquant les équations onde-plaque et les modèles de poutre/onde d'Euler-Bernoulli avec des contrôles frontières dynamiques, en utilisant la théorie des semi-groupes et l'analyse numérique. Tout d'abord, nous étudions un modèle de transmission bidimensionnel composé d'une équation des ondes et d'une équation de plaque de Kirchhoff, couplées par des conditions de transmission le long d'une interface fixe et contrôlées par trois contrôles frontières dynamiques sous certaines conditions géométriques. Bien que ce système ne soit pas exponentiellement stable, nous établissons une décroissance polynomiale de l’énergie de type 1/t pour des données initiales régulières en utilisant une approche fréquentielle combinant un raisonnement par contradiction avec la technique des multiplicateurs. Cette méthode impose des conditions géométriques particulières sur les domaines de l’onde et de la plaque. Ensuite, nous généralisons ces résultats à un modèle onde-plaque avec seulement deux contrôles frontières dynamiques au lieu des trois habituels. Notre analyse montre que cette réduction ne modifie pas le taux de décroissance polynomiale de l’énergie, qui reste de l’ordre de 1/t. Cette approche impose également des conditions géométriques spécifiques au domaine. Enfin, nous étudions la solution numérique d’un problème de transmission onde/poutre d’Euler-Bernoulli en une dimension avec contrôles frontières dynamiques. Le couplage s’effectue via des connexions aux frontières, où les équations d’onde et de poutre évoluent sur des intervalles adjacents. En utilisant la méthode des volumes finis, nous obtenons des estimations de stabilité et prouvons la convergence de la solution numérique vers la solution faible du système continu. De plus, nous présentons une expérimentation numérique validant l’étude théorique, notamment en ce qui concerne le taux de décroissance de la solution sous l'effet d’un unique contrôle frontière dynamique.
Le Patchwork de Viro est une puissante méthode de construction d'hypersurfaces algébriques réelles avec un contrôle sur la topologie. C'est d'ailleurs une des méthode les plus efficaces connues, si bien que la classe des topologies d'hypersurfaces réelles obtenues par Patchwork est aujourd'hui devenue un champs d'étude en soi. Dans la méthode du Patchwork de Viro, les topologies d'hypersurfaces réelles sont encodées de manières combinatoires, par des triangulations de polytopes à sommets entiers, duales à des hypersurfaces tropicales. Une homologie et cohomologie tropicale peut se construire sur ces objets combinatoires, c'est une homologie et cohomologie à deux indices, analogue aux groupes de Hodge en géométrie complexe. Lorsque chaque simplexe de la triangulation engendre le réseau, la triangulation est dite primitive. Philipp Jell, Kris Shaw et Jascha Smacka ont montré (2015) un théorème de dualité de Poincaré-Hodge vérifié par cette homologie et cohomologie, à coefficients réels, dans le cas d'une triangulation primitive. Puis Philipp Jell, Johanes Rau et Kris Shaw ont montré que c'était vrai lorsque l'homologie et la cohomologie étaient à coefficients dans Z (2017) et Charles Arnal, Arthur Renaudineau et Kris Shaw l'ont montré à coefficients dans Z/2Z (2019). On s'intéressera dans cet exposé à une généralisation de ce théorème aux triangulations non-primitives, lorsque l'homologie et la cohomologie tropicales sont à coefficients dans un corps de caractéristique nulle.
Soit $K$ un corps algébriquement clos de caractéristique $p\geq 0$ et soit $f\in K[[x,y]]$ une série réduite. On note $\tilde{\mathcal{O}}$ la cloture intégrale de l'anneau $\mathcal{O}:=K[[x,y]]/(f)$ et $\delta(f):=\dim_K\tilde{\mathcal{O}}/\mathcal{O}$.
Notons $$ \overline{\mu}(f):=2\delta(f)-r(f)+1 $$ où $r(f)$ est le nombre de facteurs irréductibles de $f$.
Soit $$ \mu(f):=\dim_K K[[x,y]]/\left(\frac{\partial f}{\partial x}, \frac{\partial f}{\partial y}\right). $$ le nombre de Milnor de $f$.
En 1968, Milnor a montré que $\overline{\mu}(f)=\mu(f)$ si $K=\mathbb{C}$, et en 1973, Deligne a montré qu'en toute caractéristique, $$ \mu(f)\geq\overline{\mu}(f). $$
Dans cet exposé, on s'intéresse aux cas d'égalité. (Travail commun avec Enrique Artal Bartolo.)
Polynomial diagrams (also known as containers) are a categorification of the notion of polynomial. They can be defined in any category with pullbacks, where they form a bicategory. In the setting of homotopy type theory, we show that the (wild) category of polynomial diagrams in types can be recovered as a Kleisli category over the category of spans of types, thus fitting spans and polynomials respectively as the linear and non-linear part of a homotopical model of Linear Logic. If time allows, I will talk about how this fits in a framework of infinity-categorical models of Linear Logic that we are currently developing.
We consider a system of N Brownian particles interacting through a long-range smooth potential. It is known that "propagation of chaos" holds in the mean-field scaling. Assume indeed that the initial distribution of the particles is chaotic, i.e. that the particles are independent and identically distributed. Then, for any given time, and as N becomes large, the distribution of particles remains chaotic. Moreover, the distribution of a typical particle is given by the solution of a Vlasov-Fokker-Planck equation.
In this talk, we will investigate the creation of chaos phenomenon. Starting from an initial distribution of particles which is only exchangeable, we prove that in some weak norm, propagation of chaos holds up to an error stemming from initial correlations, exponentially damped over time. This is a joint work with Armand Bernou and Mitia Duerinckx.
Soit $f : (\mathbb{R}^n, 0) \to (\mathbb{R}, 0)$ un germe de fonction définissable de classe $C^2$ et soit $(X,0) \subset (\mathbb{R}^n, 0)$ un germe d'ensemble définissable fermé. On étudie des invariants topologiques associés à $f_{\vert X}$. En particulier, on donne plusieurs formules topologiques pour des caractéristiques d'Euler. On relie aussi la topologie de $f_{\vert X}$ à la topologie d'une fonction définissable avec un point critique stratifié isolé à l'origine.
Travail en commun avec Juan Antonio Moya Pérez (Valencia).
Dans cet exposé, on va étudier des fonctions rationnelles localement bornées. C’est-à-dire, les fonctions rationnelles qui sont bornées au voisinage de chaque point de leur domaine. Ces fonctions ont déjà été étudiées de point de vue algébrique. Cependant, on va les regarder de manière géométrique. On commencera par leur caractérisation. Il existe deux points de vue équivalents de caractériser cette classe de fonctions. Le premier est celui qui vient de la lemme de sélection de courbes. Le deuxième vient de la résolution de singularités. L’observation la plus intéressante ici est que cette classe des fonctions est exactement la classe des fonctions qui peuvent être transformées en fonctions régulières ayant des valeurs dans le corps de définition (on considère ici un corps réel clos). Ensuite, on définira le lieu d’annulation d’une fonction rationnelle localement bornée. Étant donné que ces fonctions sont, en général, multi-valuées, une analyse soigneuse est nécessaire. Enfin on va démontrer une version de l’inégalité de Lojasiewicz pour cette classe de fonctions et qu’il existe, dans le cas de dimension deux une bonne correspondance entre l’algèbre et la géométrie liées à ces fonctions. Cet exposé contient des travaux réalisés en collaboration avec Victor Delage et Goulwen Fichou.
Proof complexity aims to analyse the power of formal proof systems. Specifically, it is the study of the resources required to certify the truth of mathematical statements. It plays a crucial role in computational complexity and it has close connections to circuit complexity, automated reasoning, and mathematical logic.
A key direction in proof complexity is algebraic proof complexity, which analyses proof systems that use algebraic representations of logical formulas. These systems provide insight into the power and limitations of algebraic methods in proof complexity. Among them, the Ideal Proof System (IPS), introduced by Grochow and Pitassi, is the focus of this talk. IPS represents proofs as algebraic circuits verifying the unsatisfiability of polynomial equations.
In this talk, we will explore the IPS proof system, its connections to algebraic complexity, and recent developments in its study. We will discuss lower bounds for IPS, structural properties of algebraic proofs, and their implications for classical proof complexity questions. Finally, we will highlight open problems and future directions in the field.
Travail en commun avec Chen Gong. J'expliquerai comment analyser les dégénérescences dynamiques de suites de fractions rationnelles à l'aide de la théorie de Berkovich. L'analyse non-standard joue un rôle clef dans cette approche inspirée de travaux de Yusheng Luo.
Shape optimization is a central field in applied mathematics and engineering, with applications ranging from aerodynamics to material design. The objective is to find the optimal shape of a domain that minimizes a given criterion, such as energy or resistance, while satisfying geometric constraints like fixed volume, surface area, or minimal height. Classically, solving these optimization problems requires numerical methods that rely on shape derivatives and adjoint calculations, which are computationally expensive and difficult to adapt to complex geometries. To overcome these challenges and the inherent limitations in parallelization found in classical approaches, our objective is to find a good methodology that relies on neural networks and benefits on their specific properties (easy parallelization, automatic differentiation, and a meshless approach). This requires suitable representations for both the solution of the state equation and the shape of the domain in which the equation is defined. For this purpose, we introduce the DeepRitz method to approximate solutions to the state equation and symplectic neural networks to model the domain shape effectively. We illustrate this approach through an example: minimizing the Dirichlet energy of a domain under a volume constraint. We will then propose an extention of this work for odd dimensions.
une sous-variété minimale de R^n est une sous-variété qui minimisent le volume riemannien localement autour de chaque point. Trouver des hypersurfaces algébriques minimales dans R^n pour chaque n est un problème ouvert qui a été posé par Hsiang. En 2010, Tkachev a donné une solution partielle à ce problème en montrant que l'hypersurface de n x n matrices réelles de rang n-1 est minimale. Je discuterai la généralisation suivante de ce fait : pour tout m, n et r < min(m,n), la sous-variété de m x n matrices réelles de rang r est minimale. De plus, la sous-variété de n x n matrices antisymétriques de rang 2r < n et la sous-variété de n x n matrices symétriques réelles dont les valeurs propres ont des multiplicités prescrites sont également minimales.
Abstract GSOS is a categorical framework for operational semantics, in which rules are modeled as natural transformations of a certain type. Rule systems that fit the constraints imposed by the framework are guaranteed to have desirable properties, mainly that coalgebraic behavioural equivalence, which roughly corresponds to bisimilarity, is a congruence. While bisimilarity is central in process algebra, it is far from the only notion of process equivalence of interest. However, abstract GSOS is not easily applicable to these other equivalences. This work focuses on the other extremum of the linear time-branching time spectrum (bisimilarity being the finest), namely trace equivalence. We wonder under which assumptions on abstract GSOS laws this notion of equivalence is a congruence. A study of trace equivalence for a concrete instance of abstract GSOS (to labelled transition systems with explicit termination) identifies necessary and sufficient conditions to this end. We then transpose abstract GSOS to Kleisli semantics and investigate how, with conditions on the monad (affineness) and the GSOS law (dubbed linearity and smoothness) inspired by the concrete study, trace equivalence can be shown to be a congruence.
Dans cet exposé, je commencerai par mettre en contexte une série de travaux explorant dans un sens large une méthodologie basée sur des représentations «shallow» de calculs dans Rocq. Je me concentrerai ensuite plus spécifiquement sur un travail récent qui argue que de tels interprètes monadiques construits comme des couches d'interprétation empilées sur la monade libre constituent une manière prometteuse d'implémenter et de vérifier des interprètes abstraits.
L'approche permet des preuves modulaires de la correction des interprètes résultants. Nous fournissons des combinateurs génériques de contrôle de flôt abstraits dont la correction est prouvée une fois pour toute relativement à leur contrepartie concrète. Nous démontrons comment relier des gestionnaires concrets implémentant des effets à des variantes abstraites de ces gestionnaires, en capturant essentiellement la correction habituelle des fonctions de transfert dans le contexte des interprètes monadiques. Enfin, nous fournissons des résultats génériques pour transporter les résultats de correction par interprétation des effets d'état et d'échec.
Nous avons formalisé tous les combinateurs et théories susmentionnés dans Rocq, et démontré leurs avantages en implémentant et en prouvant la correction de deux interprètes abstraits illustratifs pour un langage impératif structuré et un assembleur jouet.
Cette contribution est un travail conjoint avec Sébastien Michelland et Laure Gonnord, et a fait l'objet d'un article à ICFP'24.
Ce type de théoreme donne des conditions d'indépendance algébriques de fonctions du type $f_i(t(s))$ avec $f_i$ vérifiants des EDO très particulières et $t(s)$ des séries formelles non constantes ; par exemple :
Thm(Ax) : Pour t dans $(C[[s]]-C)^n$, si $tr.deg C( t_1, ..., t_n , exp(t_1), ... exp(t_n))/C < 1+n$ alors une combinaison Z- linéaire des t_i est constante
Thm(Pila-Tsimerman) : Pour $t$ dans $(C[[s]]-C)^n$, si $tr.deg. C( t_1, ..., t_n , j(t_1), ... j(t_n), ... j''(t_n)/C < 1+3n$ alors il existe $k<l$ et $h$ dans $PGL_2^+(Q)$ tels que $t_k = h(t_l)$.
Nous obtenons une généralisation de ces résultats en terme d'intersection improbable entre une feuille de feuilletage holomorphe (transversalement de Lie) et une sous variété algébrique. L'outil principal est la théorie de Galois des équations différentielles linéaires (Théorie de Picard-Vessiot).
Travail avec D. Blazquez-Sanz, J. Freitag et R. Nagloo
It is commonplace to split a complex, formally verified piece of software (e.g., CompCert) into a formally verified part (e.g. written in Coq/Rocq) and an unverified part (e.g., written in OCaml). There are many pitfalls when doing this (types of values exchanged, assumptions of purity, modeling of pointer equality…). We shall in particular discuss situations where the unverified part submits a result, together with an optional certificate, to a verified checker, and illustrate them with examples from the Verified Polyhedra Library and CompCert- Chamois .
We present the study of the non-linear stability of a class of travelling-wave solutions to the compressible pressureless Navier-Stokes system with a singular viscosity. These solutions encode the effect of congestion by connecting a congested left state to an uncongested right state. By using carefully weighted energy estimates we are able to prove the non-linear stability of viscous shock waves to this system under a small zero integral perturbation, which in particular extends previous results that do not handle the case where the viscosity is singular. This is a joint work with Muhammed Ali Mehmood from Imperial College, London.
Cette présentation vise à introduire un schéma monolithique GD/VF (Galerkin Discontinu/Volumes Finis) préservant les propriétés convexes (principes du maximum, positivité, entropie, ...) pour la résolution des systèmes de lois de conservation sur maillages non-structurés. Il est bien connu que les méthodes Galerkin discontinue (GD) nécessitent une limitation non linéaire pour éviter les oscillations parasites ou les instabilités non linéaires, susceptibles de provoquer l´arrêt anticipé du code de simulation. L'idée principale de ce travail est d'améliorer la robustesse des schémas GD tout en préservant autant que possible leur grande précision et leur résolution de sous-maille. Pour ce faire, une combinaison convexe entre un schéma GD d'ordre élevé et un schéma volumes finis (VF) d'ordre un sera localement effectué, à l'échelle des sous-mailles, où cela sera nécessaire. À cette fin, nous prouverons tout d'abord qu'il est possible de réécrire un schéma GD comme un schéma VF défini sur un sous-maillage, en introduisant des flux numériques spécifiques, qu'on appellera flux reconstruits GD. Le schéma monolithique GD/VF sera alors défini de la manière suivante : à chaque face de chaque sous-cellule seront assignés deux flux, un flux VF d'ordre un et un flux reconstruit d'ordre élevé, qui seront finalement combinés de manière convexe. L'objectif est alors de déterminer, par analyse, les coefficients de combinaison optimaux pour atteindre les propriétés souhaitées (par exemple, positivité, absence d´oscillations, inégalités d´entropie) tout en préservant la grande précision du schéma. Des résultats numériques sur divers types de problèmes hyperboliques seront présentés pour évaluer les performances de la méthode proposée.
Grâce à ce formalisme monolithique, nous tenterons de répondre à certaines questions : est-il possible d'assurer une stabilité entropique ? de quelle stabilité entropique parlons-nous (discrète, semi-discrète, de maille, de sous-maille, pour quelle entropie, ...) ? quels sont les coûts de telles stabilités (en terme de précision ou de perte d'autres propriétés) ? À quel point est-ce essentiel pour les problèmes qui nous intéressent ? Nous présenterons différents résultats numériques pour tenter de partiellement répondre à ces questions