Bienvenue L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, et héberge une équipe-projet Inria. Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques. L'IRIF regroupe près de deux cents personnes. Sept de ses membres ont été lauréats de l'European Research Council (ERC), trois sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences. Notion du jour Réseaux Sociaux Suivez nous sur LinkedIn, Bluesky et Mastodon : Actualités 2.6.2025 Pour Hugo Herbelin et Paul-André Melliès, le chiffre 4 semble être un porte-bonheur : pendant 4 ans, c'est à 4 qu'ils ont construit leur projet pour finalement obtenir leur bourse Synergie du programme de recherche européen (ERC). Avec Philippe de Groote et Carlos Simpson, la langue naturelle mathématique n'aura plus de secret. Rencontre et échanges avec Hugo Herbelin et Paul-André Melliès, directeurs de recherche Inria, porteurs du projet MALINCA. “Avec notre ERC, nous espérons pouvoir comprendre comment, à l'intérieur d'un texte mathématique (que l'on peut trouver dans un article, dans une page de livre de maths), qui est écrit dans ce que l'on appelle une langue naturelle (anglais, français, etc.), le texte contient en lui-même les éléments de sa correction mathématique.” 23.5.2025 Nous annonçons avec fierté que neuf papiers de dix scientifiques de l'IRIF on été selectionnés pour l'ICALP 2025! Félicitations à Pierre Fraigniaud, Frédéric Magniez, Simon Apers, Mikaël Rabie, Miklos Santha, Giannos Stamoulis, Olivier Idir, Valérie Berthé, Junyao Zhao et Thomas Colcombet. Vous pouvez retrouver ici tous les papiers acceptés edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Formath Lundi 16 juin 2025, 14 heures, 3052 Frédéric Tran Minh (LCIS Valence) A Lean-based environment for teaching proof in high-school Now pervasive in many mathematics and computer science research domains, proof assistants have recently gained importance in education, mostly during the college years. In this talk, we propose a new learning environment as a layer above the Lean proof assistant, specially targeting high-school level proofs. Inspired by other adaptations of proof assistants for teaching such as Lean-Verbose, Coq Waterproof and Proof Buddy, we designed Yalep, a declarative controlled natural language. Our aim is to reduce the number of syntactic constructions to a minimum. Inspired by coherent logic, Yale is based mainly on forward-chaining. We also provide convenience for type theory hiding, and functions defined on type subsets. We present the design choices and implementation of these features. We also designed a pedagogical progression aimed for tenth-graders about arithmetic culminating in the proof that square root of 2 is irrational. We do not teach explicitly logic and we introduce logical connectors one by one. We will test these exercises with IRIF’s interns in June. Algorithmique distribuée et graphes Mardi 17 juin 2025, 15 heures, 3052 Paweł Rzążewski (Warsaw University of Technology & University of Warsaw) H-free graphs: from structure to algorithms One of the active areas of algorithmic graph theory is to investigate how the restrictions imposed on the set of input instances influence the complexity of computational problems. Quite often we can witness an interesting interplay between graph-theoretic and algorithmic results: a good understanding on the structure of instances may help in the design of efficient algorithms. During the talk we will show some tools and techniques that can be used to develop algorithms for graphs that exclude a fixed graph F as an induced subgraph. We will mostly focus on the case that F is a path. Sémantique Mardi 17 juin 2025, 15 heures, Salle 3063 Elies Harington (LIX, École Polytechnique) ∞-categorical models of linear logic In recent years, there has been a growing interest in bicategorical models of linear logic, at first from the study of a generalization of Joyal's notion of “species of structure” (Fiore, Gambino, Hyland, Winskel), and more recently through the categorical study of game semantics (Mellies, Clairambault, Forest). Mellies' model especially uncovered how homotopical structures appear naturally when considering such game semantics.These works and more recent works on polynomial functors in Homotopy Type Theory (Finster, H, Mimram, Lucas, Seiller) have motivated the search for an ∞-categorical framework in which to fit such new models. In this presentation, after presenting the main notions from the theory of ∞-categories, I will explain how to generalize Benton's linear-non-linear adjunctions and Lafont categories to this setting, as candidates for the notion of “∞-categorical models of linear logic”. If time permits I will present examples of such models, generalizing relational and vector-space models. Algorithmes et complexité Mercredi 18 juin 2025, 11 heures, Salle 3052 Sayantan Sen (CQT, National University of Singapore) Distribution Testing in the Huge Object Model Understanding whether data generated from some experiment satisfies some property is a fundamental problem in Machine learning and Statistics. Often, the data give rise to probability distributions, and the goal is to understand some properties of these distributions by looking at only a few samples from them. However, for learning properties of high-dimensional distributions, which is widespread in practice, even reading a few samples completely is infeasible. To address this, Goldreich and Ron (ITCS 22) formalised the Huge Object Model, where the algorithm can query only a few bits from the samples. This model naturally relates to financial and medical data. In this talk, we study this model and propose some efficient algorithms to learn and test various properties of distributions in this model. This talk is based on joint works with Clément Canonne, Sourav Chakraborty, Eldar Fischer, Arijit Ghosh, Amit Levi, Gopinath Mishra, and Joy Qiping Yang, and appeared in COLT 23, STOC 25, and ITCS 25. Vérification Lundi 23 juin 2025, 11 heures, 3052 and Zoom link Sergio Yovine (Universidad ORT Uruguay) An Approach for Verifying Constrained Large Language-Models Verification of large language models is increasingly attracting attention motivated by their intended use in critical or sensible applications. In this talk we discuss a way to approach this question formally. It is based on two main elements. The first one consists in appropriately defining the composition of a language model with a controller that guides/controls its output. The second one refers to the automata-theoretic characterization of the probability distribution defined by the composition. Here, the focus is put on computing that model subject to suitable equivalence relations by means of algorithms that learn the associated congruences on strings. Like in standard model-checking frameworks, (probabilistic) temporal logic properties can be verified. Experimental results in concrete though still simple scenarios are encouraging but pinpoint interesting research challenges. Algorithmique distribuée et graphes Mardi 24 juin 2025, 15 heures 30, 3052 Hector Buffière (IRIF/ Université Paris Cité) Decomposing graphs into stable and ordered parts Automates Vendredi 27 juin 2025, 14 heures, Salle 3052 Florian Luca (Stellenbosch University) Non encore annoncé. Algorithmique distribuée et graphes Mardi 8 juillet 2025, 15 heures, 3052 Chinh T. Hoang (Wilfrid Laurier University) - Algorithmes et complexité Mercredi 9 juillet 2025, 15 heures, Salle 3071 Haotian Jiang (University of Chicago) Quasi-Monte Carlo Integration via Algorithmic Discrepancy Theory A classical approach to numerically integrating a function $f$ is Monte Carlo (MC) methods. Here, one evaluates $f$ at random points and the estimation error scales as $\sigma(f)/n^{1/2}$ with $n$ samples, where $\sigma(f)$ is the standard deviation of $f$. A different approach, widely used in practice, is using quasi-Monte Carlo (QMC) methods, where $f$ is evaluated at carefully chosen deterministic points and the error scales roughly as $1/n$. Both methods have distinctive advantages and shortcomings, and a key question has been to find a method that combines the advantages of both. In this talk, I will introduce the fascinating area of QMC methods and their connections to various areas of mathematics and to geometric discrepancy. I will then show how recent developments in algorithmic discrepancy theory can be used to give a method that combines the benefits of MC and QMC methods, and even improves upon previous QMC approaches in various ways. The talk is based on joint work with Nikhil Bansal (University of Michigan).